{"total":20,"rows":[{"id":"2109.00110","title":"MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics","created":"2021-08-31","cited_by_count":391,"area":null},{"id":"2210.12283","title":"Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs","created":"2022-10-21","cited_by_count":291,"area":null},{"id":"2205.12615","title":"Autoformalization with Large Language Models","created":"2022-05-25","cited_by_count":263,"area":null},{"id":"2202.01344","title":"Formal Mathematics Statement Curriculum Learning","created":"2022-02-03","cited_by_count":142,"area":null},{"id":"2310.00656","title":"LEGO-Prover: Neural Theorem Proving with Growing Libraries","created":"2023-10-01","cited_by_count":109,"area":null},{"id":"2404.12534","title":"Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean","created":"2024-04-18","cited_by_count":58,"area":null},{"id":"2101.06223","title":"LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning","created":"2021-01-15","cited_by_count":46,"area":null},{"id":"2102.09756","title":"TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning","created":"2021-02-19","cited_by_count":37,"area":null},{"id":"2309.15806","title":"Lyra: Orchestrating Dual Correction in Automated Theorem Proving","created":"2023-09-27","cited_by_count":25,"area":null},{"id":"2106.03906","title":"Learning to Guide a Saturation-Based Theorem Prover","created":"2021-06-07","cited_by_count":15,"area":null},{"id":"2404.07382","title":"Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving","created":"2024-04-10","cited_by_count":11,"area":null},{"id":"2111.12038","title":"Learning Symbolic Rules for Reasoning in Quasi-Natural Language","created":"2021-11-23","cited_by_count":9,"area":null},{"id":"2402.17032","title":"REFACTOR: Learning to Extract Theorems from Proofs","created":"2024-02-26","cited_by_count":9,"area":null},{"id":"2410.19940","title":"Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification","created":"2024-10-25","cited_by_count":9,"area":null},{"id":"2205.14229","title":"Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis","created":"2022-05-27","cited_by_count":5,"area":null},{"id":"2203.04699","title":"Gym-saturation: an OpenAI Gym environment for saturation provers","created":"2022-03-09","cited_by_count":3,"area":null},{"id":"2401.12131","title":"NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis","created":"2024-01-22","cited_by_count":3,"area":null},{"id":"2403.03401","title":"BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving","created":"2024-03-06","cited_by_count":2,"area":null},{"id":"2411.00863","title":"Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation","created":"2024-10-30","cited_by_count":2,"area":null},{"id":"2204.02737","title":"Adversarial Learning to Reason in an Arbitrary Logic","created":"2022-04-06","cited_by_count":1,"area":null}],"next_cursor":null}