Will Complexity theory in mathlib be mostly lambda-calculus based on 2025-02-17?
5
130Ṁ47
resolved Feb 18
Resolved
NO

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.

The Lean Theorem Prover
Computational Complexity Theory
Get
Ṁ1,000
to start trading!

🏅 Top traders

#NameTotal profit
1Ṁ15
2Ṁ1

People are also trading

Will a standardized category theory language for ML models emerge by end of 2025?
3% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
34% 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?
27% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
74% chance
Biggest formal math library in 2040 HoTT-based?
45% chance
Will an inconsistency in the Calculus of Inductive Constructions be found before 2050?
8% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
60% chance
Which theorems will be formally proven in Lean by the end of 2028?
Sort by:

Resolving NO on the basis of files like this seeming to bottom out in TMs still.

Is it easier in Lean to do that with lambda calculus?

@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.

predictedYES

@BoltonBailey you should advertise your markets on Lean's zulip, I think! They are very cool.

People are also trading

Will a standardized category theory language for ML models emerge by end of 2025?
3% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
34% 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?
27% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
74% chance
Biggest formal math library in 2040 HoTT-based?
45% chance
Will an inconsistency in the Calculus of Inductive Constructions be found before 2050?
8% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
60% chance
Which theorems will be formally proven in Lean by the end of 2028?
© Manifold Markets, Inc.•Terms•Privacy