YuanheZ/ErdosGraham

Lean

275 commits

updated Jun 3, 2026

See the code

README

Lean 4 Formalization of Irrationality of rapidly converging series: a problem of Erdős and Graham

The repo is formalized by LeanMarathon.

Inputs

source/problem.txt: target theorems statements, including Question 1 (Erdos #1051), Theorems 2, 3 & 5.
source/paper.tex: LaTeX source of paper

Output

LeanMarathon/Main.lean: completed Lean file

Proof DAG Evolution

Contributors

YuanheZ

275 commits

Similar repos

YuanheZ/LeanMarathon

A graph-engineering agent harness for long-horizon, research-level autoformalization.

same org

Pengbinghui/pipeline-math

243

epfl-lara/AutoformalizedProjects

Fully autonomous Lean formalizations of mathematical papers generated by the LeanFlow agent harness.

google-deepmind/alphaproof-nexus-results

Lean math proofs generated by AlphaProof Nexus and accompanying natural language prose proofs.

299

T3S1AMAX/autolean

AxiomMath/fel-polynomial

Lean formalizations for the paper "Fel's conjecture on syzigies of numerical semigroups"

teorth/erdosproblems

A community database for the problems on the erdosproblems.com site

860

Yuren-Tang/erdos-306

A verified Lean 4 proof of Erdős Problem 306

Languages

Lean

84.2%

Python

8.6%

TeX

7.2%

YuanheZ/ErdosGraham

Lean

275 commits

updated Jun 3, 2026

See the code

README

Lean 4 Formalization of Irrationality of rapidly converging series: a problem of Erdős and Graham

The repo is formalized by LeanMarathon.

Inputs

source/problem.txt: target theorems statements, including Question 1 (Erdos #1051), Theorems 2, 3 & 5.
source/paper.tex: LaTeX source of paper

Output

LeanMarathon/Main.lean: completed Lean file

Proof DAG Evolution

Similar repos

YuanheZ/LeanMarathon

A graph-engineering agent harness for long-horizon, research-level autoformalization.

same org

Pengbinghui/pipeline-math

243

epfl-lara/AutoformalizedProjects

Fully autonomous Lean formalizations of mathematical papers generated by the LeanFlow agent harness.

google-deepmind/alphaproof-nexus-results

Lean math proofs generated by AlphaProof Nexus and accompanying natural language prose proofs.

299

T3S1AMAX/autolean

AxiomMath/fel-polynomial

Lean formalizations for the paper "Fel's conjecture on syzigies of numerical semigroups"

teorth/erdosproblems

A community database for the problems on the erdosproblems.com site

860

Yuren-Tang/erdos-306

A verified Lean 4 proof of Erdős Problem 306

Contributors

YuanheZ

275 commits

Languages

Lean

84.2%

Python

8.6%

TeX

7.2%