Will Lean mathlib have a definition of graph minors by the end of 2024?
5
Ṁ127Ṁ1kresolved Dec 31
Resolved
NO1H
6H
1D
1W
1M
ALL
An analogous “minor map” definition exists in Coq. However, it’s up for debate whether we want to adopt that definition or something else.
This question is managed and resolved by Manifold.
Market context
Get 
1,000 to start trading!
1,000🏅 Top traders
| # | Trader | Total profit |
|---|---|---|
| 1 | Ṁ130 | |
| 2 | Ṁ12 |
People are also trading
Related questions
Will Lean mathlib contain more than 10 million lines of code by 2030?
70% chance
Which theorems will be officially formally proven in Lean by the end of 2028?
Will Fermat's last theorem proof be completely formalized in Lean in 2026?
10% chance
What tactic will prove the most mathlib lemmas at the end of 2026?