Will Lean mathlib have a definition of graph minors by the end of 2024? | Manifold

Will Lean mathlib have a definition of graph minors by the end of 2024?

Mini

5

Ṁ158

Dec 31

80%

chance

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.

️ Technology Math The Lean Theorem Prover

Get Ṁ1,000 play money

Sort by:

Betting YES because I'm gonna do it.

Related questions

Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?

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?

Related questions

Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?

Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?

What tactic will prove the most mathlib lemmas at the end of 2026?