[HN Gopher] Automatic Textbook Formalization
       ___________________________________________________________________
        
       Automatic Textbook Formalization
        
       Author : tzury
       Score  : 21 points
       Date   : 2026-04-03 20:13 UTC (2 hours ago)
        
 (HTM) web link (github.com)
 (TXT) w3m dump (github.com)
        
       | tzury wrote:
       | More details:
       | https://x.com/FabianGloeckle/status/2040082785851904401
        
         | mkl wrote:
         | That just shows the first post for most people. Here is all of
         | it:
         | https://xcancel.com/FabianGloeckle/status/204008278585190440...
        
       | alex_be wrote:
       | Big step toward AI-assisted mathematical research
        
       | auggierose wrote:
       | Which LLMs do these agents use?
        
         | auggierose wrote:
         | Claude Opus 4.5
        
       | measurablefunc wrote:
       | This is a lot of useful data for the next iteration of Claude
       | because not only does Anthropic have the final artifacts but they
       | also saw the entire workflow from start to finish & Facebook paid
       | them for the privilege of giving them all of that training data.
        
       | smj-edison wrote:
       | It's interesting to see a lot of formalized proofs gather around
       | Lean (specifically Mathlib). I've in a formal math class right
       | now, so it's a bit weird learning ZFC while messing around with
       | Lean, which is based on dependant types.
       | 
       | There's a lot of other proof assistants out there, like Mizar,
       | Isabelle, Metamath, Metamath0, and Coq, each based on different
       | foundations. Metamath0 in particular looks really intriguing,
       | since it's the brainchild of Mario Carneiro, who was also the
       | person who started Mathlib (and I believe is still an active
       | contributor).
       | 
       | Anyways, Lean definitely has a lot going for it, but I love to
       | tinker, and it's interesting to see other proof assistants' takes
       | on things.
        
       ___________________________________________________________________
       (page generated 2026-04-03 23:00 UTC)