Will Complexity theory in mathlib be mostly lambda-calculus based on 2025-02-17?
5
130Ṁ47resolved Feb 18
Resolved
NO1D
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,000 to start trading!
1,000🏅 Top traders
| # | Name | Total profit |
|---|---|---|
| 1 | Ṁ15 | |
| 2 | Ṁ1 |
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
Related questions
What tactic will prove the most mathlib lemmas at the end of 2026?
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
41% chance
Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
19% chance
Will LLMs be able to formally verify non-trivial programs by the end of 2025?
31% chance
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
65% chance
Will an inconsistency in the Calculus of Inductive Constructions be found before 2050?
9% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
60% chance
Will ZFC no longer be the standard foundation for mathematics by 2050?
33% chance