When will LLMs be able to generate formal proof for sudoku solver?
Mini
4
Ṁ1132027
1D
1W
1M
ALL
16%
2024
37%
2025
24%
2026
23%
2027 or later
When LLMs or hybrid AI models can generate both the implementation of a Sudoku solver and its formal specification, along with a formal proof of correctness?
Prompts might look like: 'Write a Sudoku solver in Coq and formally prove its correctness.'
Model should be generally available
Get Ṁ1,000 play money
Related questions
Related questions
When will we have a fully formalized proof of Fermat's Last Theorem?
Will LLMs solve the first 15 days of Advent of Code?
53% chance
Will the best public LLM at the end of 2025 solve more than 5 of the first 10 Project Euler problems published in 2026?
42% chance
In 2029, will any AI be able to take an arbitrary proof in the mathematical literature and translate it into a form suitable for symbolic verification? (Gary Marcus benchmark #5)
70% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
69% chance
Will there be any simple text-based task that most humans can solve, but top LLMs can't? By the end of 2026
64% chance
By 2028 will we be able to identify distinct submodules/algorithms within LLMs?
75% chance
Will an LLM be able to solve a Rubik's Cube by 2025?
69% chance
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
59% chance
Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?
48% chance