{"total":21,"rows":[{"id":"2406.16838","title":"From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models","created":"2024-06-24","cited_by_count":137,"area":null},{"id":"2406.03847","title":"Lean Workbook: A large-scale Lean problem set formalized from natural language math problems","created":"2024-06-06","cited_by_count":122,"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":"2404.09939","title":"A Survey on Deep Learning for Theorem Proving","created":"2024-04-15","cited_by_count":57,"area":null},{"id":"2408.03350","title":"miniCTX: Neural Theorem Proving with (Long-)Contexts","created":"2024-08-05","cited_by_count":37,"area":null},{"id":"2312.07622","title":"Mathematical Language Models: A Survey","created":"2023-12-12","cited_by_count":24,"area":null},{"id":"2406.11915","title":"miniCodeProps: a Minimal Benchmark for Proving Code Properties","created":"2024-06-16","cited_by_count":18,"area":null},{"id":"2506.11085","title":"LeanExplore: A search engine for Lean 4 declarations","created":"2025-06-04","cited_by_count":18,"area":null},{"id":"2505.24264","title":"Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations","created":"2025-05-30","cited_by_count":8,"area":null},{"id":"2510.15940","title":"Lean Finder: Semantic Search for Mathlib That Understands User Intents","created":"2025-10-08","cited_by_count":8,"area":null},{"id":"2406.15540","title":"Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods","created":"2024-06-21","cited_by_count":6,"area":null},{"id":"2411.02318","title":"Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast","created":"2024-11-04","cited_by_count":5,"area":null},{"id":"2410.15748","title":"Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation","created":"2024-10-21","cited_by_count":4,"area":null},{"id":"2501.13959","title":"Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization","created":"2025-01-21","cited_by_count":4,"area":null},{"id":"2502.15507","title":"Steering LLMs for Formal Theorem Proving","created":"2025-02-21","cited_by_count":4,"area":null},{"id":"2503.09730","title":"Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving","created":"2025-03-12","cited_by_count":2,"area":null},{"id":"2502.04671","title":"ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving","created":"2025-02-07","cited_by_count":1,"area":null},{"id":"2504.19188","title":"Hierarchical Attention Generates Better Proofs","created":"2025-04-27","cited_by_count":1,"area":null},{"id":"2607.07779","title":"From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier","created":"2026-07-08","cited_by_count":1,"area":null},{"id":"2510.11944","title":"TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition","created":"2025-10-13","cited_by_count":0,"area":null},{"id":"2606.26490","title":"An Empirical Study of LLM-Generated Specifications for VeriFast","created":"2026-06-25","cited_by_count":0,"area":null}],"next_cursor":null}