Real functions
The Lean Pool projects whose card's first MSC2020 code is in class 26, Real functions: 1 article.
TheoremArchon-FirstProof-Results#
Problem4.harmonic_mean_inequality_full Problem6.exists_eps_light_subset
Collects formal solutions from the Archon FirstProof benchmark, including polynomial and graph-theoretic results.
Quoted from the card LeanPool/projects/archon-firstproof-results.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
Main results
The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Problem4.harmonic_mean_inequality_full(theorem; a main declaration), declared in LeanPool/ArchonFirstProofResults/FirstProof4/Problem4.lean, line 878: “Proves the benchmark harmonic-mean inequality for real-rooted polynomial transforms.”Problem6.exists_eps_light_subset(theorem; a main declaration), declared in LeanPool/ArchonFirstProofResults/FirstProof6/Problem6.lean, line 1319: “Proves the benchmark light-subset existence theorem in the graph Laplacian setting.”
Project
Project
- Authors: FrenzyMath.
- Source: arXiv:2602.05192.
- Project repository: frenzymath/Archon-FirstProof-Results.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 26D15, 05C50, 15A42.
- In Lean Pool: LeanPool/ArchonFirstProofResults, from the card LeanPool/projects/archon-firstproof-results.yaml.
Sources
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.