EFX allocations do not exist for n ≥ 3 agents and m ≥ n+5 goods with monotone valuations; a counterexample is constructed via SAT solving and the encoding is verified in Lean.
hub
The Lean mathematical library
37 Pith papers cite this work, alongside 124 external citations. Polarity classification is still indexing.
37
Pith papers citing it
124
external citations · external index
hub tools
citation-role summary
background 3
citation-polarity summary
roles
background 3polarities
background 3representative citing papers
Introduces LCS-Bench, a theory-scale benchmark covering 327 textbook items and 4,076 Lean declarations, with evaluations showing state-of-the-art models reach only 20.1% on auto-formalization tasks.
TheoremBench is a Lean4 benchmark of classical theorems in main and premised forms that evaluates LLM provers on partial progress, coverage, and token efficiency rather than binary success on competition problems.
Machine learning methods discover a new noncrossing-partition statistic interpreting q,t-Narayana polynomials and yield a combinatorial proof of their symmetry.
MathAtlas is the first large-scale benchmark for autoformalizing graduate mathematics, where even strong models reach only 9.8% correctness on theorem statements and drop to 2.6% on the hardest dependency-deep subset.
A Lean 4 formalization of Gröbner basis theory that uniformly handles arbitrary and infinite numbers of variables with verified division, Buchberger criterion, and reduced bases.
MiniF2F is a new cross-system benchmark containing 488 Olympiad-level mathematics problems formalized in Metamath, Lean, Isabelle, and HOL Light, together with baseline results from a GPT-3-based prover.
LAMP achieves 96.7% success generating verified Lean proofs for 90 Combinatorics on Words theorems by coordinating Planner, Builder, and Verifier agents with a CoW ontology accessed through Model Context Protocol.
Proofs depending on the axiom of choice show a geometric signature in neural embeddings of tactic sequences that weakens with dependency-graph distance and correlates with prover failure rates.
AXLE is a multi-tenant cloud platform providing Lean 4 metaprogramming utilities with per-request isolation, multi-version support, and public access via SDK and API, having processed over 500 million requests.
Introduces Relaxed NFL intermediate language for LLM-based auto-formalization, with rule-plus-LLM elaboration to Core NFL and tactic-language discharge of verification conditions.
Proves R(B_8, B_10) = 37 via an AI-assisted short proof with a Lean formalization of the upper bound.
A new Lean tactic automates bitvector-finite field equivalence proofs and solves 19% more ZKP arithmetization benchmarks than state-of-the-art SMT solvers.
Formal Conjectures is a Lean 4 benchmark containing 2615 formalized problems with 1029 open conjectures, designed to evaluate automated mathematical reasoning and proof discovery.
LeanSearch v2 recovers 46.1% of ground-truth premise groups for research-level Lean 4 theorems within 10 candidates and raises fixed-loop proof success to 20%.
A SAT-plus-LLM method discovers infinite families of doubly saturated Ramsey-good graphs, answering Grinstead and Roberts' 1982 question.
LeetProof achieves higher rates of fully certified program synthesis from natural language by using a multi-modal verifier in Lean to validate specifications via randomized testing and delegate proofs to AI tools, outperforming single-mode baselines on benchmarks while uncovering defects in prior参考.
Machine-checked formalization in Lean 4 of the Wu-Ritt method with proofs that characteristic sets and zero decompositions correctly capture the solution sets of polynomial systems.
The CHSH rigidity theorem is machine-checked in Lean 4, confirming near-optimal strategies are locally isometric to the qubit strategy while exposing a gap in prior reasoning.
ImProver is an LLM agent using Chain-of-States, error-correction, and retrieval to rewrite Lean proofs for arbitrary user-defined optimization criteria like shortness and readability.
A 400-entry benchmark and protocol shows tool-augmented agents reach 89.5% compilation but only 60.5% consensus faithfulness, with a 29-point gap; elaboration feedback improves validity most but increases unfaithful compiles.
Formalizes line search methods, conditions, and Zoutendijk theorem in Lean 4 to support verified nonlinear optimization.
Lean 4 formalization of q-ary covering code theory with certificate predicates for bounds on K_q(n,r) and a proof-carrying database of upper and lower bounds.
Agent-directed tree search improves LLM performance on Lean formal verification tasks, with context-based orchestration solving more intermediate specs at lower token cost than baseline agents.
citing papers explorer
-
A Counterexample to EFX $n \ge 3$ Agents, $m \ge n + 5$ Items, Submodular Valuations via SAT-Solving
EFX allocations do not exist for n ≥ 3 agents and m ≥ n+5 goods with monotone valuations; a counterexample is constructed via SAT solving and the encoding is verified in Lean.
-
Theory-Scale Auto-Formalization of Logics for Computer Science
Introduces LCS-Bench, a theory-scale benchmark covering 327 textbook items and 4,076 Lean declarations, with evaluations showing state-of-the-art models reach only 20.1% on auto-formalization tasks.
-
TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics
TheoremBench is a Lean4 benchmark of classical theorems in main and premised forms that evaluates LLM provers on partial progress, coverage, and token efficiency rather than binary success on competition problems.
-
Mapping Uncharted Symmetries: Machine Discovery in Combinatorics
Machine learning methods discover a new noncrossing-partition statistic interpreting q,t-Narayana polynomials and yield a combinatorial proof of their symmetry.
-
MathAtlas: A Benchmark for Autoformalization in the Wild
MathAtlas is the first large-scale benchmark for autoformalizing graduate mathematics, where even strong models reach only 9.8% correctness on theorem statements and drop to 2.6% on the hardest dependency-deep subset.
-
Formalizing Gr\"obner Basis Theory in Lean
A Lean 4 formalization of Gröbner basis theory that uniformly handles arbitrary and infinite numbers of variables with verified division, Buchberger criterion, and reduced bases.
-
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
MiniF2F is a new cross-system benchmark containing 488 Olympiad-level mathematics problems formalized in Metamath, Lean, Isabelle, and HOL Light, together with baseline results from a GPT-3-based prover.
-
LAMP: Lean-based Agentic framework with MCP and Proof Repair
LAMP achieves 96.7% success generating verified Lean proofs for 90 Combinatorics on Words theorems by coordinating Planner, Builder, and Verifier agents with a CoW ontology accessed through Model Context Protocol.
-
Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings
Proofs depending on the axiom of choice show a geometric signature in neural embeddings of tactic sequences that weakens with dependency-graph distance and correlates with prover failure rates.
-
AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities
AXLE is a multi-tenant cloud platform providing Lean 4 metaprogramming utilities with per-request isolation, multi-version support, and public access via SDK and API, having processed over 500 million requests.
-
Verifiable Auto-Formalization of Mathematics Using a Relaxed Natural Formal Language
Introduces Relaxed NFL intermediate language for LLM-based auto-formalization, with rule-plus-LLM elaboration to Core NFL and tactic-language discharge of verification conditions.
-
An automated proof that R(B_8,B_10)=37
Proves R(B_8, B_10) = 37 via an AI-assisted short proof with a Lean formalization of the upper bound.
-
Automating Bitvector and Finite Field Equivalence Proofs in Lean
A new Lean tactic automates bitvector-finite field equivalence proofs and solves 19% more ZKP arithmetization benchmarks than state-of-the-art SMT solvers.
-
Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
Formal Conjectures is a Lean 4 benchmark containing 2615 formalized problems with 1029 open conjectures, designed to evaluate automated mathematical reasoning and proof discovery.
-
LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
LeanSearch v2 recovers 46.1% of ground-truth premise groups for research-level Lean 4 theorems within 10 candidates and raises fixed-loop proof success to 20%.
-
Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery
A SAT-plus-LLM method discovers infinite families of doubly saturated Ramsey-good graphs, answering Grinstead and Roberts' 1982 question.
-
Certified Program Synthesis with a Multi-Modal Verifier
LeetProof achieves higher rates of fully certified program synthesis from natural language by using a multi-modal verifier in Lean to validate specifications via randomized testing and delegate proofs to AI tools, outperforming single-mode baselines on benchmarks while uncovering defects in prior参考.
-
Formalizing Wu-Ritt Method in Lean 4
Machine-checked formalization in Lean 4 of the Wu-Ritt method with proofs that characteristic sets and zero decompositions correctly capture the solution sets of polynomial systems.
-
Formalizing CHSH Rigidity in Lean 4
The CHSH rigidity theorem is machine-checked in Lean 4, confirming near-optimal strategies are locally isometric to the qubit strategy while exposing a gap in prior reasoning.
-
ImProver: Agent-Based Automated Proof Optimization
ImProver is an LLM agent using Chain-of-States, error-correction, and retrieval to rewrite Lean proofs for arbitrary user-defined optimization criteria like shortness and readability.
-
Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
A 400-entry benchmark and protocol shows tool-augmented agents reach 89.5% compilation but only 60.5% consensus faithfulness, with a 29-point gap; elaboration feedback improves validity most but increases unfaithful compiles.
-
Formalization of Line Search Methods by Lean
Formalizes line search methods, conditions, and Zoutendijk theorem in Lean 4 to support verified nonlinear optimization.
-
Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4
Lean 4 formalization of q-ary covering code theory with certificate predicates for bounds on K_q(n,r) and a proof-carrying database of upper and lower bounds.
-
Automating Formal Verification with Agent-Guided Tree Search
Agent-directed tree search improves LLM performance on Lean formal verification tasks, with context-based orchestration solving more intermediate specs at lower token cost than baseline agents.
-
Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
A machine-checked Lean 4 formalization of Stokes' theorem on smooth singular cubes with true Fréchet pullback, chain-level extensions, and comparison to prior HOL Light work.
-
Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game
The Obfuscated Natural Number Game shows reasoning LLMs keep proof accuracy without semantic cues while general models degrade, establishing a metric for architectural reasoning in alien math domains.
-
A Minimal Agent for Automated Theorem Proving
A minimal agentic system achieves competitive performance in automated theorem proving with a simpler design and lower cost than state-of-the-art methods.
-
StarCoder 2 and The Stack v2: The Next Generation
StarCoder2-15B matches or beats CodeLlama-34B on code tasks despite being smaller, and StarCoder2-3B outperforms prior 15B models, with open weights and exact training data identifiers released.
-
Llemma: An Open Language Model For Mathematics
Continued pretraining of Code Llama on Proof-Pile-2 yields Llemma, an open math-specialized LLM that beats known open base models on MATH and supports tool use plus formal proving out of the box.
-
Vector alignment in matrix Lie groups
Vector alignment for all classical matrix Lie groups via pseudoinverse, log, Lie-algebra projection, and exponential, with a quasi-Newton correction for noisy data.
-
Topology as Logic: Structural Role Geometry Across Formal, Software, Biological, and Prebiotic Systems
Pre-registered multilayer network tests across seven substrates show betweenness-based hub persistence recovers expert-described logic structures better than degree, with confirmed correlations in ISCAS85 and Lean mathlib4.
-
Automating Formal Verification with Reinforcement Learning and Recursive Inference
RLVR training raises verified Dafny pass rates from 9.7% to 31.1% on a filtered benchmark while a Lean proof scaffold lifts success from 46.2% to 69.2% on a pilot set and solves 7 of 42 prior unsolved tasks.
-
Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs
MathArena is broadened into a maintained platform with new benchmarks for proofs, research questions, and formal verification, where GPT-5.5 scores 98% on 2026 USAMO and 74% on research-level tasks.
-
Automated Tactics for Polynomial Reasoning in Lean 4
Develops certificate-based tactics in Lean 4 that import and formally verify Gröbner basis results from external computer algebra systems for polynomial ideal problems.
-
Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)
Advocates logical pluralism at the object level inside a unifying HOL meta-framework to enable interdisciplinary reuse and warns against single-logic imperialism.
- Automating Boundary Filling in Cubical Type Theories
- Univalent Enriched Categories and the Enriched Rezk Completion