:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Liu, Junqi, Zhou, Zihao, Zhu, Zekai, Santos, Marco Dos, He, Weikun, Liu, Jiawei, Wang, Ran, Xie, Yunzhou, Zhao, Junqiao, Wang, Qiufeng, Zhi, Lihong, Li, Jia, Li, Wenda
Format:	Preprint
Published:	2026
Subjects:	Artificial Intelligence
Online Access:	https://arxiv.org/abs/2601.14027
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A Formal Proof of the Irrationality of $ζ(3)$ in Lean 4
by: Liu, Junqi, et al.
Published: (2025)

Formalizing Gröbner Basis Theory in Lean
by: Guo, Junyu, et al.
Published: (2026)

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

Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification
by: Santos, Marco Dos, et al.
Published: (2025)

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

Formalizing Wu-Ritt Method in Lean 4
by: Xiao, Yuxuan, et al.
Published: (2026)

CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization
by: Peng, Zhongyuan, et al.
Published: (2025)

CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics
by: Liu, Junqi, et al.
Published: (2025)

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

Is Your Model Really A Good Math Reasoner? Evaluating Mathematical Reasoning with Checklist
by: Zhou, Zihao, et al.
Published: (2024)

Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs
by: Xiong, Beibei, et al.
Published: (2026)

An Algorithm for Diagonalizing Matrices of Formal Power Series
by: Dai, Zihao, et al.
Published: (2026)

Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
by: Qiu, Ruichen, et al.
Published: (2026)

OpenHA: A Series of Open-Source Hierarchical Agentic Models in Minecraft
by: Wang, Zihao, et al.
Published: (2025)

A Formally Verified Library of Mathematical Finance in Lean 4
by: Coelho, Raphael
Published: (2026)

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models
by: Yu, Zhouliang, et al.
Published: (2025)

Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
by: Wang, Haiming, et al.
Published: (2025)

Can MLLMs Absorb Math Reasoning Abilities from LLMs as Free Lunch?
by: Hu, Yijie, et al.
Published: (2025)

Whitney Stratification of Algebraic Boundaries of Convex Semi-algebraic Sets
by: Dai, Zihao, et al.
Published: (2024)

Allocating Mixed Goods with Customized Fairness and Indivisibility Ratio
by: Li, Bo, et al.
Published: (2024)

Rethinking Wireless Communications through Formal Mathematical AI Reasoning
by: Zhao, Changyuan, et al.
Published: (2026)

Hierarchical Alignment: Enforcing Hierarchical Instruction-Following in LLMs through Logical Consistency
by: Yang, Shu, et al.
Published: (2026)

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

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

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

Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
by: Baba, Kaito, et al.
Published: (2025)

LeanAgent: Lifelong Learning for Formal Theorem Proving
by: Kumarappan, Adarsh, et al.
Published: (2024)

Open-Ended Video Game Glitch Detection with Agentic Reasoning and Temporal Grounding
by: Zheng, Muyang, et al.
Published: (2026)

Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4
by: Tang, Xichen
Published: (2024)

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

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4
by: Yang, Bowen, et al.
Published: (2026)

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

Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4
by: Li, Yuxin, et al.
Published: (2025)

FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean
by: Meadows, Jordan, et al.
Published: (2026)

Sketch2MinSurf: Vision-Language Guided Generation of Editable Minimal Surfaces from Hand-Drawn Sketches
by: Wang, Wenda, et al.
Published: (2026)

ViRC: Enhancing Visual Interleaved Mathematical CoT with Reason Chunking
by: Wang, Lihong, et al.
Published: (2025)

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

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

A Formal Approach to AMM Fee Mechanisms with Lean 4
by: Dessalvi, Marco, et al.
Published: (2026)

Biofouling prevention and control technology for marine engineering equipment: from traditional methods to intelligent interface engineering.
by: Wang, Juncheng, et al.
Published: (2026)