Copertina

Process-Driven Autoformalization in Lean 4

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Lu, Jianqiao, Wan, Yingjia, Liu, Zhengying, Huang, Yinya, Xiong, Jing, Liu, Chengwu, Shen, Jianhao, Jin, Hui, Zhang, Jipeng, Wang, Haiming, Yang, Zhicheng, Tang, Jing, Guo, Zhijiang
Natura:	Preprint
Pubblicazione:	2024
Soggetti:	Computation and Language Machine Learning Logic in Computer Science
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

FormalAlign: Automated Alignment Evaluation for Autoformalization
di: Lu, Jianqiao, et al.
Pubblicazione: (2024)

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

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

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

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

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

Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
di: Yin, David, et al.
Pubblicazione: (2025)

Improving the Diproche CNL through Autoformalization via Large Language Models
di: Carl, Merlin
Pubblicazione: (2023)

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

ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization
di: Cabral, Rafael, et al.
Pubblicazione: (2025)

Autoformalizing Euclidean Geometry
di: Murphy, Logan, et al.
Pubblicazione: (2024)

Can Large Language Models Autoformalize Kinematics?
di: Kabra, Aditi, et al.
Pubblicazione: (2025)

Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents
di: Brown, Chad E., et al.
Pubblicazione: (2026)

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

Lean-SMT: An SMT tactic for discharging proof goals in Lean
di: Mohamed, Abdalrhman, et al.
Pubblicazione: (2025)

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

Munkres' General Topology Autoformalized in Isabelle/HOL
di: Bryant, Dustin, et al.
Pubblicazione: (2026)

Aligning with Logic: Measuring, Evaluating and Improving Logical Preference Consistency in Large Language Models
di: Liu, Yinhong, et al.
Pubblicazione: (2024)

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

Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection
di: Lalwani, Abhinav, et al.
Pubblicazione: (2024)

130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?
di: Urban, Josef
Pubblicazione: (2026)

Intuitionistic Propositional Logic in Lean
di: Trufaş, Dafina
Pubblicazione: (2024)

Lean on Vampire Proofs (Short Paper)
di: Bodingbauer, Jonas, et al.
Pubblicazione: (2026)

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

AutoPSV: Automated Process-Supervised Verifier
di: Lu, Jianqiao, et al.
Pubblicazione: (2024)

Towards Autoformalization of LLM-generated Outputs for Requirement Verification
di: Gupte, Mihir, et al.
Pubblicazione: (2025)

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

Sequencelib: A Computational Platform for Formalizing the OEIS in Lean
di: Moreira, Walter, et al.
Pubblicazione: (2026)

LeanArchitect: Automating Blueprint Generation for Humans and AI
di: Zhu, Thomas, et al.
Pubblicazione: (2026)

Automating Bitvector and Finite Field Equivalence Proofs in Lean
di: Pertseva, Elizaveta, et al.
Pubblicazione: (2026)

ZFLean: a framework for set-level mathematics in Lean
di: Trélat, Vincent
Pubblicazione: (2026)

SFT-GRPO Data Overlap as a Post-Training Hyperparameter for Autoformalization
di: Su, Xiaole, et al.
Pubblicazione: (2026)

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

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

Synthetic Differential Geometry in Lean
di: Brasca, Riccardo, et al.
Pubblicazione: (2026)

FlexProofs: A Vector Commitment with Flexible Linear Time for Computing All Proofs
di: Liu, Jing, et al.
Pubblicazione: (2026)

Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4
di: Mayeux, Arnaud, et al.
Pubblicazione: (2026)

DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
di: Rowney, Tate, et al.
Pubblicazione: (2026)

CSLib: The Lean Computer Science Library
di: Barrett, Clark, et al.
Pubblicazione: (2026)

Unbiasing symmetric monoidal categories in Lean
di: Carlier, Robin
Pubblicazione: (2026)