Skip to content

PROBLEMS.md

Latest commit

 

History

History
93 lines (52 loc) · 3.8 KB

PROBLEMS.md

File metadata and controls

93 lines (52 loc) · 3.8 KB
Raw

FormalQualBench: curated research theorem list

This catalog is intentionally research-level (no IMO/Putnam/etc.). It mainly focuses on theorem statements for proven results in the literature that are not currently available as a finished Lean/Mathlib theorem, with the benchmark surface intended to stay on mathematically established results rather than unsolved conjectures.

Each checked item corresponds to a single Lean stub at FormalQualBench/<Name>/Main.lean containing only the necessary definitions/imports + a main statement with a by sorry proof.

Curation signals

  • Mathlib proof_wanted declarations (known results with missing proofs in Lean)
  • Famous results whose statements can be expressed using existing Mathlib definitions (even if the proof is far out of reach)

Current problems

Topology / geometry

  • Borsuk–Ulam theorem (FormalQualBench/BorsukUlamTheorem/Main.lean)

Topology / geometric functional analysis

  • Banach–Stone theorem (FormalQualBench/BanachStoneTheorem/Main.lean)

Logic / model theory

  • Quantifier elimination for dense linear orders without endpoints (DLO) (FormalQualBench/DLOQuantifierElimination/Main.lean)

Logic / Ramsey theory

  • Paris-Harrington principle (strengthened finite Ramsey theorem) (FormalQualBench/ParisHarringtonPrinciple/Main.lean)

Number theory

  • Maynard-Tao bounded prime gaps theorem (FormalQualBench/MaynardTaoBoundedPrimeGaps/Main.lean)
  • Helfgott's ternary Goldbach theorem (FormalQualBench/TernaryGoldbachTheorem/Main.lean)

Algebra / group theory

  • Jordan theorem: primitive groups containing a prime cycle contain Aₙ (FormalQualBench/JordanCycleTheorem/Main.lean)
  • Jordan derangement theorem for finite transitive permutation groups (FormalQualBench/JordanDerangementTheorem/Main.lean)
  • Burnside theorem for permutation groups of prime degree (FormalQualBench/BurnsidePrimeDegreeTheorem/Main.lean)

Algebra / commutative algebra

  • Quillen–Suslin theorem (Serre’s conjecture) (FormalQualBench/QuillenSuslinTheorem/Main.lean)

Algebra / real algebraic geometry

  • Artin’s solution to Hilbert’s 17th problem (FormalQualBench/Hilbert17thProblem/Main.lean)

Analysis / complex analysis

  • Gleason-Kahane-Zelazko theorem (FormalQualBench/GleasonKahaneZelazkoTheorem/Main.lean)
  • Runge’s theorem (polynomial approximation on compact sets) (FormalQualBench/RungeTheorem/Main.lean)

Additive combinatorics / analytic number theory

  • Tao's solution of the Erdős discrepancy problem (FormalQualBench/ErdosDiscrepancyProblem/Main.lean)
  • Green-Tao theorem on arithmetic progressions in the primes (FormalQualBench/GreenTaoTheorem/Main.lean)

Analysis / operator algebras

  • von Neumann double commutant theorem (FormalQualBench/VonNeumannDoubleCommutantTheorem/Main.lean)

Topological groups / harmonic analysis

  • Pontryagin duality via the canonical evaluation map (FormalQualBench/PontryaginDuality/Main.lean)

Combinatorics / graph theory

  • De Bruijn–Erdős theorem (compactness for graph coloring) (FormalQualBench/DeBruijnErdos/Main.lean)

Combinatorial / convex geometry

  • Colorful Carathéodory theorem (FormalQualBench/ColorfulCaratheodoryTheorem/Main.lean)

Harmonic analysis / geometric measure theory

  • Three-dimensional Kakeya theorem (FormalQualBench/KakeyaTheorem3D/Main.lean)

Analysis / fixed point theory

  • Schauder fixed point theorem (FormalQualBench/SchauderFixedPointTheorem/Main.lean)

Arithmetic dynamics / recurrence sequences

  • Skolem-Mahler-Lech theorem (FormalQualBench/SkolemMahlerLechTheorem/Main.lean)

Dynamical systems / arithmetic

  • Almost-bounded values for the Collatz map (FormalQualBench/CollatzMapAlmostBoundedValues/Main.lean)