About whether AI can formalize mathematics like algebraic topology in Lean.
Has this happened?
Yes 38 (34%)Not sure 59 (53%)No 15 (13%)
Votes cast 1–2 October 2026: 100,590 votes from 9,694 people.
Hacker News has set AI a lot of challenges over the years. Which ones has it met?
About whether AI can formalize mathematics like algebraic topology in Lean.
Votes cast 1–2 October 2026: 100,590 votes from 9,694 people.
You'd think with all those billions spent on the software and the hardware it would be a walk in the park to convert a single book on algebraic topology into a formalized Coq, Lean, or Isabelle module. Seems like a very obvious test case for the intelligence capabilities of these systems. I know that it is possible because Kevin Buzzard is going to formalize Fermat's last theorem for less than £934,043 but no commercial AI lab has yet managed to build an AI that can do basic arithmetic. [0] Mira Murati is on the record about their next AI model and that it will have the intelligence of a PhD student so let's see if their next model can actually formalize basic algebraic topology into a logical calculus. [1]
0: https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/Y0...
1: https://engineering.dartmouth.edu/news/openai-cto-mira-murat...