Will Complexity theory in mathlib be mostly lambda-calculus based on 2025-02-17?
Basic
4
Ṁ37Feb 17
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.
This question is managed and resolved by Manifold.
Get
1,000and
3.00
1,0003.00Sort 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
Related questions
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
59% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
40% chance
Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?
89% chance
Will we have any progress on the interpretability of State Space Model LLM’s in 2024?
71% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
69% chance
Will ZFC no longer be the standard foundation for mathematics by 2050?
33% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will a Millenium problem be formally stated in a theorem prover by 2025
59% chance
Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
19% chance
Will an AI be able to convert recent mathematical results into a fully formal proofs that can be verified by a mainstream proof assistant by 2025?
5% chance