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

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

🏅 Top traders

#TraderTotal profit
1Ṁ15
2Ṁ1

People are also trading

Will Fermat's last theorem proof be completely formalized in Lean in 2026?
12% 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?
44% chance
Will Lean mathlib contain more than 10 million lines of code by 2030?
67% chance
Which theorems will be officially formally proven in Lean by the end of 2028?
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
Will ZFC no longer be the standard foundation for mathematics by 2050?
33% chance
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 Fermat's last theorem proof be completely formalized in Lean in 2026?
12% 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?
44% chance
Will Lean mathlib contain more than 10 million lines of code by 2030?
67% chance
Which theorems will be officially formally proven in Lean by the end of 2028?
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
Will ZFC no longer be the standard foundation for mathematics by 2050?
33% chance
© Manifold Markets, Inc.•Terms•Privacy