Will Complexity theory in mathlib be mostly lambda-calculus based on 2025-02-17?
4
62
Ṁ38Ṁ130
2025
63%
chance
1D
1W
1M
ALL
On the close date I will inspect the mathlib code-base to find theorems related to computational complexity theory. I will then try to assess whether the model of computation in these theorems is best described as a form of the lambda calculus (rather than models like Turing machines or RAM). If most of the theorems are based on lambda calcului, I will resolve YES, otherwise NO.
Get Ṁ200 play money
Sort by:
@wadimiusz Currently I believe the only computational model is TM-based, but a group of mathlib developers have been discussing the use of lambda-calculus and I believe most of them think it would be easier. See this thread for discussion.
@BoltonBailey you should advertise your markets on Lean's zulip, I think! They are very cool.
Related questions
Will AIs be widely recognized as having developed a new, innovative, foundational mathematical theory before 2030?
42% chance
Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?
63% chance
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
59% chance
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
60% chance
Will reinforcement learning overtake LMs on math before 2028?
43% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
42% 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?
65% chance
Will ZFC no longer be the standard foundation for mathematics by 2050?
34% chance
Will AIs be widely recognized as having developed a new, innovative, foundational mathematical theory before 2035?
49% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
65% chance