Pith. sign in

REVIEW 5 cited by

LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2407.17227 v1 pith:NLNIWFFI submitted 2024-07-24 cs.AI cs.CL

Zijian Wu , Jiayu Wang , Dahua Lin , Kai Chen This is my paper · ORCID
classification cs.AIcs.CL
keywords formalleandatadatasetgithublanguagelean-githubcorpora
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

Recently, large language models have presented promising results in aiding formal mathematical reasoning. However, their performance is restricted due to the scarcity of formal theorem-proving data, which requires additional effort to be extracted from raw formal language corpora. Meanwhile, a significant amount of human-written formal language corpora remains underutilized. To address this issue, we propose LEAN-GitHub, a dataset consisting of large-scale formal data extracted from almost all Lean 4 repositories on GitHub. After fine-tuning InternLM-math-plus on this dataset, our model achieved accuracies of 48.8% with a single pass and 54.5% with 64 passes on the Lean 4 miniF2F test, surpassing state-of-the-art method at 52%. And it also achieves state-of-the-art on two other Lean 4 benchmarks (ProofNet and Putnam) targeting different fields/levels of math. These results demonstrate that our proposed dataset is beneficial for formal reasoning on a wide range of math topics. We open-source our model at https://GitHub. com/InternLM/InternLM-Math and our data at https://huggingface.co/ datasets/InternLM/Lean-GitHub

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 5 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

    cs.CL 2026-07 accept novelty 6.0 of 10

    LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.

  2. Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

    cs.AI 2025-07 conditional novelty 6.0 of 10

    Seed-Prover and Seed-Geometry prove 121 of 155 formalized past IMO problems, reach 99.6% on MiniF2F-test, and solve 5 of 6 IMO 2025 problems after the competition deadline.

  3. Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models

    cs.AI 2025-06 conditional novelty 6.0 of 10

    An inference-only neuro-symbolic pipeline, DSP+, solves 80.7% of miniF2F and the previously unsolved imo_2019_p1, matching heavily RL-trained theorem provers without fine-tuning.

  4. Integrating Rules and Semantics for LLM-Based C-to-Rust Translation

    cs.SE 2025-08 unverdicted novelty 5.0 of 10

    IRENE combines rule-based retrieval, structured summarization, and compiler feedback to improve LLM-based C-to-Rust translation accuracy and safety.

  5. Solving Formal Math Problems by Decomposition and Iterative Reflection

    cs.AI 2025-07 conditional novelty 5.0 of 10

    An agent that decomposes Lean 4 goals into subproblems and iteratively repairs proofs achieves a 95.9% pass rate on miniF2F-test using a stock Gemini model.

Pith tools