:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Li, Yuxin, Liu, Minghao, Wang, Ruida, Ji, Wenzhao, He, Zhitao, Pan, Rui, Huang, Junming, Zhang, Tong, Fung, Yi R.
Format:	Preprint
Published:	2025
Subjects:	Artificial Intelligence Machine Learning
Online Access:	https://arxiv.org/abs/2510.26094
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4
by: Yao, Jiarui, et al.
Published: (2025)

TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
by: Wang, Ruida, et al.
Published: (2024)

MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
by: Wang, Ruida, et al.
Published: (2025)

Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capability
by: Wang, Ruida, et al.
Published: (2025)

MedEBench: Diagnosing Reliability in Text-Guided Medical Image Editing
by: Liu, Minghao, et al.
Published: (2025)

LeanGeo: Formalizing Competitional Geometry problems in Lean
by: Song, Chendong, et al.
Published: (2025)

LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
by: Gao, Guoxiong, et al.
Published: (2026)

LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4
by: Kripner, Matěj, et al.
Published: (2025)

LeanExplore: A search engine for Lean 4 declarations
by: Asher, Justin
Published: (2025)

Lean4Lean: Verifying a Typechecker for Lean, in Lean
by: Carneiro, Mario
Published: (2024)

An Evaluation Benchmark for Autoformalization in Lean4
by: Gulati, Aryan, et al.
Published: (2024)

Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models
by: Guo, Dadi, et al.
Published: (2025)

MAC-Tuning: LLM Multi-Compositional Problem Reasoning with Enhanced Knowledge Boundary Awareness
by: Huang, Junsheng, et al.
Published: (2025)

RebuttalAgent: Strategic Persuasion in Academic Rebuttal via Theory of Mind
by: He, Zhitao, et al.
Published: (2026)

Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning
by: Bourigault, Pauline, et al.
Published: (2026)

PBLean: Pseudo-Boolean Proof Certificates for Lean 4
by: Szeider, Stefan
Published: (2026)

PhysProver: Advancing Automatic Theorem Proving for Physics
by: Zhang, Hanning, et al.
Published: (2026)

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
by: Shen, Ziju, et al.
Published: (2025)

Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
by: Liu, Junqi, et al.
Published: (2026)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
by: Song, Peiyang, et al.
Published: (2024)

Automated Tactics for Polynomial Reasoning in Lean 4
by: Shen, Hao, et al.
Published: (2026)

SELF-REDRAFT: Eliciting Intrinsic Exploration-Exploitation Balance in Test-Time Scaling for Code Generation
by: Chen, Yixiang, et al.
Published: (2025)

LeanReasoner: Boosting Complex Logical Reasoning with Lean
by: Jiang, Dongwei, et al.
Published: (2024)

APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
by: Ospanov, Azim, et al.
Published: (2025)

LLMs' Leaning in European Elections
by: Ricciuti, Federico
Published: (2025)

Herald: A Natural Language Annotated Lean 4 Dataset
by: Gao, Guoxiong, et al.
Published: (2024)

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
by: Liu, Chengwu, et al.
Published: (2026)

MerLean: An Agentic Framework for Autoformalization in Quantum Computation
by: Ren, Yuanjie, et al.
Published: (2026)

Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4
by: Shen, Austin, et al.
Published: (2026)

Political Leaning and Politicalness Classification of Texts
by: Volf, Matous, et al.
Published: (2025)

LeanC2: Lean 4 formalization for the C2
by: Motta, Thiago F.
Published: (2026)

Process-Driven Autoformalization in Lean 4
by: Lu, Jianqiao, et al.
Published: (2024)

Distilling LLM Feedback for Lean Theorem Proving
by: Narozniak, Gaetan, et al.
Published: (2026)

Formally Solving Answer-Construction Problems in Lean
by: Sun, Jialiang, et al.
Published: (2025)

Premise Selection for a Lean Hammer
by: Zhu, Thomas, et al.
Published: (2025)

GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving
by: Wang, Ruida, et al.
Published: (2025)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
by: Qian, Yicheng, et al.
Published: (2025)

Less is More: Lean yet Powerful Vision-Language Model for Autonomous Driving
by: Yang, Sheng, et al.
Published: (2025)

LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)
by: Xu, Rongge, et al.
Published: (2025)

Lean-STaR: Learning to Interleave Thinking and Proving
by: Lin, Haohan, et al.
Published: (2024)