Comment Re:This will push formalisation into the mainstrea (Score 4, Informative) 31
AI can easily write the lean for any proofs they do. The problem is that lean is missing large parts of established mathematics.
My current lean project has to cite all of these externally due to missing lean support.
Functional equations / means
- lit_aczel_1948 — Aczél: symmetric + homogeneous means power/quasi-arithmetic mean (the CES forcing)
- lit_aczel_1966_weighted — weighted Aczél characterization (weighted means)
Fixed-point / topology
- lit_brouwer_1911 — Brouwer fixed point
- lit_cellina_approximate_selection_1969 — approximate selection (closed-graph correspondences); with Brouwer
Kakutani
- lit_glicksberg_1952 — Glicksberg fixed point (infinite/Bayesian games)
- lit_berge_maximum_theorem_1959 — Berge maximum theorem (upper-hemicontinuity)
Probability / large deviations
- lit_sanov_1957 — Sanov / method of types (large-deviation rate = KL)
- lit_fisher_tippett_gnedenko_1928 — extreme-value theorem (GEV limit laws)
- lit_kolmogorov_1931_fokker_planck — Fokker–Planck diffusion equation
Optimal transport / matching
- lit_sinkhorn_1967 — Sinkhorn matrix scaling (entropic OT)
- lit_lp_strong_duality_1951 — LP / transportation strong duality (Gale–Kuhn–Tucker)
- lit_entropic_penalty_cominetti_sanmartin_1994 — entropic-penalty -convergence (T0)
- lit_gale_shapley_1962 — deferred acceptance produces a stable matching
- lit_gale_shapley_proposer_optimal_1962 — proposer-optimality of deferred acceptance
Stochastic calculus / PDE
- lit_ito_1944 — Itô's lemma
- lit_black_scholes_pde_solution_1973 — closed-form solution of the Black–Scholes PDE
- lit_liouville_dirichlet — Liouville/Dirichlet (harmonic-function / PDE result)
Dynamical systems
- lit_saddlenode_passage_time — saddle-node "bottleneck" passage time / (Strogatz/Fenichel)
