Buchumschlag

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Zhang, Terry Jingchen, Jiang, Wenyuan, Liu, Rongchuan, Wang, Yisong, Yang, Junran, Wang, Ning, Ni, Nicole, Huang, Yinya, Sachan, Mrinmaya
Format:	Preprint
Veröffentlicht:	2025
Schlagworte:	Logic in Computer Science Artificial Intelligence Computation and Language Machine Learning
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

LeanAgent: Lifelong Learning for Formal Theorem Proving
von: Kumarappan, Adarsh, et al.
Veröffentlicht: (2024)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
von: Li, Jinzheng, et al.
Veröffentlicht: (2026)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
von: Song, Peiyang, et al.
Veröffentlicht: (2024)

Canonical for Automated Theorem Proving in Lean
von: Norman, Chase, et al.
Veröffentlicht: (2025)

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

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
von: Aniva, Leni, et al.
Veröffentlicht: (2026)

What are the Right Symmetries for Formal Theorem Proving?
von: Olejniczak, Krzysztof, et al.
Veröffentlicht: (2026)

Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
von: Liu, Qi, et al.
Veröffentlicht: (2025)

Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4
von: Baek, Jineon, et al.
Veröffentlicht: (2024)

An In-Context Learning Agent for Formal Theorem-Proving
von: Thakur, Amitayush, et al.
Veröffentlicht: (2023)

Equational Theorem Proving for Clauses over Strings
von: Kim, Dohan
Veröffentlicht: (2023)

Formalizing Automated Market Makers in the Lean 4 Theorem Prover
von: Pusceddu, Daniele, et al.
Veröffentlicht: (2024)

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

Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
von: Florath, Andreas
Veröffentlicht: (2024)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
von: Qian, Yicheng, et al.
Veröffentlicht: (2025)

Automated Theorem Proving for Prolog Verification
von: Mesnard, Fred, et al.
Veröffentlicht: (2026)

Formalizing Wu-Ritt Method in Lean 4
von: Xiao, Yuxuan, et al.
Veröffentlicht: (2026)

Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization
von: Yanahama, Banri, et al.
Veröffentlicht: (2026)

LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Game
von: Kabra, Aditi, et al.
Veröffentlicht: (2026)

Sequencelib: A Computational Platform for Formalizing the OEIS in Lean
von: Moreira, Walter, et al.
Veröffentlicht: (2026)

Partial Label Learning for Automated Theorem Proving
von: Zombori, Zsolt, et al.
Veröffentlicht: (2025)

Process-Driven Autoformalization in Lean 4
von: Lu, Jianqiao, et al.
Veröffentlicht: (2024)

CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems
von: Ji, Junye
Veröffentlicht: (2026)

Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs
von: Yousefzadeh, Roozbeh, et al.
Veröffentlicht: (2025)

Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
von: Rao, Balaji, et al.
Veröffentlicht: (2025)

Formalizing CHSH Rigidity in Lean 4
von: Zhao, Tianrun, et al.
Veröffentlicht: (2026)

A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations (Extended Version)
von: Ge, Rui, et al.
Veröffentlicht: (2024)

Formalizing $A_1^{(1)}$ Curve Neighborhoods in Lean 4
von: Huang, Yihe, et al.
Veröffentlicht: (2026)

Translating Informal Proofs into Formal Proofs Using a Chain of States
von: Wang, Ziyu, et al.
Veröffentlicht: (2025)

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

LeanBET: Formally-verified surface area calculations in Lean
von: Ugwuanyi, Ejike D., et al.
Veröffentlicht: (2026)

The Chase in Lean -- Crafting a Formal Library for Existential Rule Research
von: Gerlach, Lukas
Veröffentlicht: (2026)

Formalizing Representation Theorems for a Logical Framework with Rewriting
von: Traversié, Thomas, et al.
Veröffentlicht: (2025)

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

Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
von: Aniva, Leni, et al.
Veröffentlicht: (2024)

Proving Behavioural Apartness
von: Turkenburg, Ruben, et al.
Veröffentlicht: (2024)

3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
von: Lamont, Sean, et al.
Veröffentlicht: (2024)

SubgoalXL: Subgoal-based Expert Learning for Theorem Proving
von: Zhao, Xueliang, et al.
Veröffentlicht: (2024)

Formalizing Gröbner Basis Theory in Lean
von: Guo, Junyu, et al.
Veröffentlicht: (2026)

BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
von: Lamont, Sean, et al.
Veröffentlicht: (2024)