Biggest formal math library in 2040 HoTT-based?
2
Ṁ100Ṁ252040
44%
chance
1H
6H
1D
1W
1M
ALL
I am thinking of projects like unimath, mathlib or mathcomp. "Biggest" to be defined in terms of number of theorems from the 1000+ theorems project that have been formally proven in the library.
This question is managed and resolved by Manifold.
Market context
Get 
1,000 to start trading!
1,000People are also trading
Related questions
What tactic will prove the most mathlib lemmas at the end of 2026?
Will Fermat's last theorem proof be completely formalized in Lean in 2026?
12% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
60% chance
Will Lean mathlib contain more than 10 million lines of code by 2030?
69% chance