Cover Image

Herald: A Natural Language Annotated Lean 4 Dataset

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Gao, Guoxiong, Wang, Yutong, Jiang, Jiedong, Gao, Qi, Qin, Zihan, Xu, Tianyi, Dong, Bin
Format:	Preprint
Published:	2024
Subjects:	Computation and Language Artificial Intelligence Machine Learning Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

A Semantic Search Engine for Mathlib4
by: Gao, Guoxiong, et al.
Published: (2024)

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

FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
by: Jiang, Jiedong, et al.
Published: (2025)

Compositional Consistency-Guided Decoding for Three-Way Logical Question Answering
by: Huang, Tianyi, et al.
Published: (2026)

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

DECIDER: A Dual-System Rule-Controllable Decoding Framework for Language Generation
by: Xu, Chen, et al.
Published: (2024)

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

ASP-Bench: From Natural Language to Logic Programs
by: Szeider, Stefan
Published: (2026)

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

Combining Textual and Structural Information for Premise Selection in Lean
by: Petrovčič, Job, et al.
Published: (2025)

Can Large Language Models Understand DL-Lite Ontologies? An Empirical Study
by: Wang, Keyu, et al.
Published: (2024)

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

Llemma: An Open Language Model For Mathematics
by: Azerbayev, Zhangir, et al.
Published: (2023)

A Neurosymbolic Approach to Natural Language Formalization and Verification
by: Bayless, Sam, et al.
Published: (2025)

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

Towards Logically Sound Natural Language Reasoning with Logic-Enhanced Language Model Agents
by: Mensfelt, Agnieszka, et al.
Published: (2024)

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

Defining implication relation for classical logic
by: Fu, Li
Published: (2013)

Generics and Default Reasoning in Large Language Models
by: Kirkpatrick, James Ravi, et al.
Published: (2025)

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

Multi-Step Deductive Reasoning Over Natural Language: An Empirical Study on Out-of-Distribution Generalisation
by: Bao, Qiming, et al.
Published: (2022)

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

Reasoning Capabilities of Large Language Models. Lessons Learned from General Game Playing
by: Świechowski, Maciej, et al.
Published: (2026)

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

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

RvLLM: LLM Runtime Verification with Domain Knowledge
by: Zhang, Yedi, et al.
Published: (2025)

Nl2Hltl2Plan: Scaling Up Natural Language Understanding for Multi-Robots Through Hierarchical Temporal Logic Task Representation
by: Xu, Shaojun, et al.
Published: (2024)

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

Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
by: Lu, Jialin, et al.
Published: (2026)

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

Premise Selection for a Lean Hammer
by: Zhu, Thomas, et al.
Published: (2025)

Advancing Spatial Reasoning in Large Language Models: An In-Depth Evaluation and Enhancement Using the StepGame Benchmark
by: Li, Fangjun, et al.
Published: (2024)

Token Assorted: Mixing Latent and Text Tokens for Improved Language Model Reasoning
by: Su, DiJia, et al.
Published: (2025)

Soda: An Object-Oriented Functional Language for Specifying Human-Centered Problems
by: Mendez, Julian Alfredo
Published: (2023)

Lattice Annotated Temporal (LAT) Logic for Non-Markovian Reasoning
by: Mukherji, Kaustuv, et al.
Published: (2025)

Modeling Next-Token Prediction as Left-Nested Intuitionistic Implication
by: Tarau, Paul
Published: (2026)

Where to Search: Measure the Prior-Structured Search Space of LLM Agents
by: Song, Zhuo-Yang
Published: (2025)

Logic-Parametric Neuro-Symbolic NLI: Controlling Logical Formalisms for Verifiable LLM Reasoning
by: Farjami, Ali, et al.
Published: (2026)

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