Will Terence Tao write a paper with Lean code in it during the 2026 calendar year?
8
58
Ṁ76Ṁ210
2027
74%
chance
1D
1W
1M
ALL
Fields medalist Terence Tao has recently been interested in the Lean proof assistant. He recently started formalizing one of his papers in Lean.
This question is to forecast whether he will still be interested in Lean in a few years. It resolves YES if Tao publishes or preprints any paper with Lean source code in the text of the paper between 2026-01-01 and 2026-12-31.
Get Ṁ200 play money
Related questions
Will Manifold be cited in a paper from a top-tier AI lab or AI journal before 2025?
45% chance
Will Diana Leung publish an academic paper in 2024?
59% chance
Will an AI produce encyclopedia-worthy philosophy by 2026?
20% chance
Will a Large Language Model be listed as an author on a peer-reviewed paper by the end of 2025?
48% chance
Will @HastingsGreer coauthor an ICML or NeurIPS paper in 2024?
50% chance
Will Kevin Buzzard successfully formalize Fermat's Last Theorem in Lean within his 5 year grant?
66% chance
Will an algorithm be able to work on million-line codebases before 2026?
70% chance
Will Anthropic and OpenAI collaborate substantially on a research paper before 2025?
51% chance
Will an AI generate a blog post indistinguishable from Robin Hanson's writing if tested before 2026?
70% chance
Will AI contribute as much as a co-author would today to a real research mathematics paper before Jan 1 2025?
33% chance