Copertina

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Yang, Bowen, Yuan, Yi, Li, Chenyi, Wang, Ziyu, Li, Liangqi, Zhang, Bo, Li, Zhe, Wen, Zaiwen
Natura:	Preprint
Pubblicazione:	2026
Soggetti:	Logic in Computer Science
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

Translating Informal Proofs into Formal Proofs Using a Chain of States
di: Wang, Ziyu, et al.
Pubblicazione: (2025)

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

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

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

CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
di: Long, Wentao, 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)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
di: Mohamed, Abdalrhman, 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)

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

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

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

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

Limited Math: Aligning Mathematical Semantics with Finite Computation
di: Wen, Lian
Pubblicazione: (2026)

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

Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics
di: Ambridge, Todd Waugh
Pubblicazione: (2024)

A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs
di: Watanabe, Kazuki, et al.
Pubblicazione: (2025)

Formalizing CHSH Rigidity in Lean 4
di: Zhao, Tianrun, et al.
Pubblicazione: (2026)

Formal Verification of Parameterized Systems based on Induction
di: Xiu, Jiaqi, et al.
Pubblicazione: (2025)

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

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

Formalizing $A_1^{(1)}$ Curve Neighborhoods in Lean 4
di: Huang, Yihe, et al.
Pubblicazione: (2026)

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

On the Cut Elimination of Weak Intuitionistic Tense Logic
di: Wang, Yiheng, et al.
Pubblicazione: (2024)

LeanTutor: Towards a Verified AI Mathematical Proof Tutor
di: Patel, Manooshree, et al.
Pubblicazione: (2025)

Constructive Ordinal Exponentiation
di: de Jong, Tom, et al.
Pubblicazione: (2025)

Constructive Quantum Logics
di: Aguilera, Juan P., et al.
Pubblicazione: (2025)

Meta-Mathematics of Computational Complexity Theory
di: Oliveira, Igor C.
Pubblicazione: (2025)

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)

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

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

CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems
di: Ji, Junye
Pubblicazione: (2026)

The Complexity of the Constructive Master Modality
di: Santiago-Fernández, Sofía, et al.
Pubblicazione: (2026)

Blurred Drinker Paradoxes and Blurred Choice Axioms: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem
di: Kirst, Dominik, et al.
Pubblicazione: (2026)

FORWORD: Accelerating Formal Datapath Verification via Word-Level Sweeping
di: Yang, Ziyi, et al.
Pubblicazione: (2025)

Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4
di: Baek, Jineon, et al.
Pubblicazione: (2024)

An Analysis of Tennenbaum's Theorem in Constructive Type Theory
di: Hermes, Marc, et al.
Pubblicazione: (2023)

Constructive higher sheaf models with applications to synthetic mathematics
di: Coquand, Thierry, et al.
Pubblicazione: (2026)