Cover Image

MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Liu, Xinyu, Xie, Zixuan, Moeini, Amir, Chen, Claire, Liu, Shuze Daniel, Meng, Yu, Zhang, Aidong, Zhang, Shangtong
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Artificial Intelligence Machine Learning
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries
by: Xie, Zixuan, et al.
Published: (2026)

Lemmas: Generation, Selection, Application
by: Rawson, Michael, et al.
Published: (2023)

Lemmanaid: Neuro-Symbolic Lemma Conjecturing
by: Alhessi, Yousef, et al.
Published: (2025)

Affine Disjunctive Invariant Generation with Farkas' Lemma
by: Ke, Jingyu, et al.
Published: (2023)

A Beluga Formalization of the Harmony Lemma in the $π$-Calculus
by: Cecilia, Gabriele, et al.
Published: (2024)

A New Kim's Lemma
by: Kruckman, Alex, et al.
Published: (2023)

MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification
by: Li, Sirui, et al.
Published: (2025)

Non-Archimedean Analogue of Chase's Lemma
by: Mihara, Tomoki
Published: (2026)

Well-Founded Coalgebras Meet König's Lemma
by: Urbat, Henning, et al.
Published: (2025)

Borel Local Lemma: arbitrary random variables and limited exponential growth
by: Bernshteyn, Anton, et al.
Published: (2024)

Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
by: Peled, Romy, et al.
Published: (2025)

Feasibly Constructive Proof of Schwartz-Zippel Lemma and the Complexity of Finding Hitting Sets
by: Atserias, Albert, et al.
Published: (2024)

A Formalization of the Generalized Quantum Stein's Lemma in Lean
by: Meiburg, Alex, et al.
Published: (2025)

The ODE Method for Stochastic Approximation and Reinforcement Learning with Markovian Noise
by: Liu, Shuze Daniel, et al.
Published: (2024)

Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL
by: Hulak, David B., et al.
Published: (2026)

Linear $Q$-Learning Does Not Diverge in $L^2$: Convergence Rates to a Bounded Set
by: Liu, Xinyu, et al.
Published: (2025)

Learning Formal Mathematics From Intrinsic Motivation
by: Poesia, Gabriel, et al.
Published: (2024)

Beyond Linear Attention: Softmax Transformers Implement In-Context Reinforcement Learning
by: Xie, Zixuan, et al.
Published: (2026)

Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT
by: Civini, Emanuele, et al.
Published: (2026)

A Simple and Elementary Proof of Zorn's Lemma
by: Nuida, Koji
Published: (2023)

An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction
by: Xu, Yang, et al.
Published: (2025)

Doubly Optimal Policy Evaluation for Reinforcement Learning
by: Liu, Shuze Daniel, et al.
Published: (2024)

Efficient Multi-Policy Evaluation for Reinforcement Learning
by: Liu, Shuze Daniel, et al.
Published: (2024)

Efficient Policy Evaluation with Safety Constraint for Reinforcement Learning
by: Chen, Claire, et al.
Published: (2024)

ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers
by: Chen, Chen, et al.
Published: (2025)

Formal Mathematical Reasoning: A New Frontier in AI
by: Yang, Kaiyu, et al.
Published: (2024)

A motivic Fundamental Lemma
by: Forey, Arthur, et al.
Published: (2023)

Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs
by: Yousefzadeh, Roozbeh, et al.
Published: (2025)

A Semantic Search Engine for Mathlib4
by: Gao, Guoxiong, et al.
Published: (2024)

Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
by: Liu, Qi, et al.
Published: (2025)

Borel versions of the Local Lemma and LOCAL algorithms for graphs of finite asymptotic separation index
by: Bernshteyn, Anton, et al.
Published: (2023)

From Blind Solvers to Logical Thinkers: Benchmarking LLMs' Logical Integrity on Faulty Mathematical Problems
by: Rahman, A M Muntasir, et al.
Published: (2024)

Finite Sample Analysis of Linear Temporal Difference Learning with Arbitrary Features
by: Xie, Zixuan, et al.
Published: (2025)

Efficient Policy Evaluation with Offline Data Informed Behavior Policy Design
by: Liu, Shuze, et al.
Published: (2023)

Rethinking Explanations: Formalizing Contrast in Description Logics
by: Mahmood, Yasir, et al.
Published: (2026)

Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
by: Dougherty, Quinn, et al.
Published: (2025)

Compression is all you need: Modeling Mathematics
by: Aksenov, Vitaly, et al.
Published: (2026)

Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
by: Edmonds, Chelsea, et al.
Published: (2023)

A Theory of Formalisms for Representing Knowledge
by: Zhang, Heng, et al.
Published: (2024)

Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques
by: Han, Sangjun, et al.
Published: (2025)