About whether LLMs plus backtracking search could prove mathematical theorems, after OpenAI's rumored breakthrough.
Has this happened?
Yes 65 (58%)Not sure 36 (32%)No 12 (11%)
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 LLMs plus backtracking search could prove mathematical theorems, after OpenAI's rumored breakthrough.
Votes cast 1–2 October 2026: 100,590 votes from 9,694 people.
There are certainly efforts along the lines of what you suggest. There are problems though. The number of backtracks is 10^k where k is not 2, or 3, or 4.....
Another issue is that of autoformalisation. This is the one part of the problem where an LLM might be able to help, if it were reliable enough (it isn't currently) or if it could truly understand the logical structure of mathematical problems correctly (currently they can't).