[HN Gopher] Terence Tao: At the Erdos problem website, AI assist...
       ___________________________________________________________________
        
       Terence Tao: At the Erdos problem website, AI assistance now
       becoming routine
        
       Author : dwohnitmok
       Score  : 137 points
       Date   : 2025-11-22 20:27 UTC (1 days ago)
        
 (HTM) web link (mathstodon.xyz)
 (TXT) w3m dump (mathstodon.xyz)
        
       | RossBencina wrote:
       | Also interesting that the responses include anti-Lean material.
        
         | CamperBob2 wrote:
         | Due to his position and general fame, Tao has to deal with a
         | larger-than-usual number of kooks.
        
         | orochimaaru wrote:
         | I'm not a mathematician, but how credible is that anti-Lean
         | material? Are they marketing an alternative programmatic
         | approach, as in they're anti-lean because "I got something
         | else" or are they philosophically anti-Lean and have valid
         | arguments?
        
         | testartr wrote:
         | gemini take on the anti-lean material:
         | 
         | Based on the document provided, this is not "crank material"
         | (in the sense of being incoherent nonsense or anti-
         | intellectual), but rather a radical philosophical critique
         | rooted in Finitism or Ultrafinitism.
         | 
         | The document makes a coherent argument, but it relies on a
         | specific philosophical view that rejects the standard
         | foundations of modern mathematics (ZFC Set Theory).
         | 
         | The arguments heavily echo the views of mathematicians like
         | Doron Zeilberger (explicitly linked in the document) and strict
         | Formalists. Zeilberger is a well-known, prize-winning
         | mathematician who famously argues that infinity does not exist
         | and that computers should just manipulate finite symbols.
        
       | kregasaurusrex wrote:
       | 'Vibe formalizing' is a logical extension of 'vibe engineering'
       | implemented by 'vibe coding'. Sometimes I have trouble with
       | getting the individual puzzle pieces of a problem to fall into
       | place, where a hypothetical 'Move 37 As A Service' to unify
       | informal methods with mathematical rigor deserves to be explored!
        
       | NitpickLawyer wrote:
       | Having the ability to throw math heavy ML papers at the
       | assistants and get simplified explanations / pseudocode back is
       | absolutely amazing, as someone who's forgot most of what I
       | learned in uni, 25+ years back and never really used it since.
        
       | xhkkffbf wrote:
       | They should name one of the AI's "Erdos". Then we can all have an
       | Erdos number of one!
        
         | hatmatrix wrote:
         | There is an AI-integrated IDE called Erdos...
         | 
         | https://www.lotas.ai/erdos
        
       | adidoit wrote:
       | I hope we continue to see gains for scientific professionals and
       | companies doing research.
       | 
       | Even imperfect assistants increase leverage.
        
       | WhyOhWhyQ wrote:
       | I've had mixed results with AI on research mathematics. I've
       | gotten it to auto-complete non-trivial arguments, and I've found
       | some domains where it seems hopelessly lost. I think we're still
       | at a point in history where mathematicians will not be replaced
       | by AI and can only benefit by dabbling with it.
        
       ___________________________________________________________________
       (page generated 2025-11-23 23:00 UTC)