Copertina

Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autore principale:	Tang, Xichen
Natura:	Preprint
Pubblicazione:	2024
Soggetti:	Computation and Language
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
di: Tang, Xichen
Pubblicazione: (2025)

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

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
di: Li, Jinzheng, et al.
Pubblicazione: (2026)

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

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

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
di: Zhang, Terry Jingchen, et al.
Pubblicazione: (2025)

Steering LLMs for Formal Theorem Proving
di: Kirtania, Shashank, et al.
Pubblicazione: (2025)

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

OProver: A Unified Framework for Agentic Formal Theorem Proving
di: Ma, David, et al.
Pubblicazione: (2026)

An In-Context Learning Agent for Formal Theorem-Proving
di: Thakur, Amitayush, et al.
Pubblicazione: (2023)

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

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

Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training
di: Zhou, Xinyuan, et al.
Pubblicazione: (2025)

Benchmarking Testing in Automated Theorem Proving
di: Kim, Jongyoon, et al.
Pubblicazione: (2026)

Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
di: Rao, Balaji, et al.
Pubblicazione: (2025)

Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving
di: Cao, Chuxue, et al.
Pubblicazione: (2025)

FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving
di: Lin, Xiaohan, et al.
Pubblicazione: (2024)

MathEDU: Feedback Generation on Problem-Solving Processes for Mathematical Learning Support
di: Hsu, Wei-Ling, et al.
Pubblicazione: (2025)

FMC: Formalization of Natural Language Mathematical Competition Problems
di: Xie, Jiaxuan, et al.
Pubblicazione: (2025)

Automated Theorem Proving for Prolog Verification
di: Mesnard, Fred, et al.
Pubblicazione: (2026)

Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
di: Zhao, Jianhong, et al.
Pubblicazione: (2025)

Aristotle: IMO-level Automated Theorem Proving
di: Achim, Tudor, et al.
Pubblicazione: (2025)

Canonical for Automated Theorem Proving in Lean
di: Norman, Chase, et al.
Pubblicazione: (2025)

A Theorem-Proving-Based Evaluation of Neural Semantic Parsing
di: Funakura, Hayate, et al.
Pubblicazione: (2025)

Does Learning Mathematical Problem-Solving Generalize to Broader Reasoning?
di: Zhou, Ruochen, et al.
Pubblicazione: (2025)

RLMEval: Evaluating Research-Level Neural Theorem Proving
di: Poiroux, Auguste, et al.
Pubblicazione: (2025)

Lyra: Orchestrating Dual Correction in Automated Theorem Proving
di: Zheng, Chuanyang, et al.
Pubblicazione: (2023)

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

Learning to Reason with Insight for Informal Theorem Proving
di: Li, Yunhe, et al.
Pubblicazione: (2026)

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

Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations
di: Quan, Xin, et al.
Pubblicazione: (2025)

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
di: Chen, Luoxin, et al.
Pubblicazione: (2025)

Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving
di: Quan, Xin, et al.
Pubblicazione: (2024)

DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
di: Zhang, Ziyin, et al.
Pubblicazione: (2025)

miniCTX: Neural Theorem Proving with (Long-)Contexts
di: Hu, Jiewen, et al.
Pubblicazione: (2024)

MathGLM-Vision: Solving Mathematical Problems with Multi-Modal Large Language Model
di: Yang, Zhen, et al.
Pubblicazione: (2024)

Formalization of Auslander--Buchsbaum--Serre criterion in Lean4
di: Guan, Naillin, et al.
Pubblicazione: (2025)

Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving
di: Li, Vincent, et al.
Pubblicazione: (2025)

LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
di: Onda, Naoto, et al.
Pubblicazione: (2025)

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