1. CircuitProver: Agentic Lean 4 Theorem Proving with Reusable Circuit Proof Library for Hardware Verification
   2026/07/29 by Ziyi Yang, Wenji Fang, Chen Chen +2 · 1 voice
   Computer Science · #cs.LO #cs.AR
2. Completeness of Canonical Closure Representations Is coNP-Complete
   2026/07/20 by Mikhail Babin · 1 voice
   #cs.DM #cs.CC #cs.LO
3. Quantifying Diversity of Thought: A Predictive Law of Weighted LLM Ensemble Lift
   2026/07/19 by Junade Ali · 1 citation
   #cs.AI #cs.LG #cs.LO #cs.MA
4. The Σ-Chain Product: A Succinct Model of Automata (De)Composition (Extended Version)
   2026/07/18 by Roberto Borelli, Davide Bresolin, Luca Geatti +2 · 1 voice
   #cs.FL #cs.LO
5. 3-VASS Reachability is in EXPSPACE
   2026/07/16 by Weijun Chen, Bo Fu, Yuxi Fu +4 · 1 voice
   #cs.FL #cs.LO
6. Rzk: a Proof Assistant for Synthetic ∞-Categories
   2026/07/13 by Nikolai Kudasov, Violetta Sim, Benedikt Ahrens · 1 voice
   #cs.LO #cs.PL #math.CT
7. Bidirectional Elaborators à la Carte
   2026/07/10 by Andrew Slattery, Jonathan Sterling · 2 voices
   #cs.PL #cs.LO
8. Kani: A Model Checker for Rust
   2026/07/01 by Rémi Delmas, Zyad Hassan, Qinheping Hu +9 · 11 voices
   #cs.SE #cs.LO #cs.PL
9. A Machine-Verified Proof of a Quantum-Optimization Conjecture
   2026/06/29 by Uri Kol, Maor Ben-Shahar, Kfir Sulimany +1 · 2 voices
   Physics and Astronomy · Computer Science · Mathematics · #quant-ph #cs.AI #cs.LG #cs.LO #math.OC
10. Lattice Deduction Transformers
    2026/05/09 by Liam Davis, Leopold Haller, Alberto Alfarano +1 · 1 voice
    #cs.LG #cs.AI #cs.LO
11. Inexpressibility in Exp-Minus-Log
    2026/05/02 by Mark Carney · 3 voices
    #math.LO #cs.LO
12. Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
    2026/03/09 by Joseph Tooby-Smith · 8 voices · 1 citation
    #hep-ph #cs.LO #hep-th
13. Toward Guarantees for Clinical Reasoning in Vision Language Models via Formal Verification
    2026/02/27 by Vikash Singh, Debargha Ganguly, Haotian Yu +5 · 2 voices
    #cs.CV #cs.AI #cs.CL #cs.LO
14. RustyDL: A Program Logic for Rust
    2026/02/25 by Daniel Drodt, Reiner Hähnle · 1 voice
    Computer Science · #cs.PL #cs.LO
15. CSLib: The Lean Computer Science Library
    2026/02/04 by Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi +5 · 5 voices
    #cs.LO #cs.PL
16. interwhen: A Generalizable Framework for Steering Reasoning Models with Test-time Verification
    2026/02/05 by Vishak K Bhat, Prateek Chanda, Vijval Ekbote +6 · 2 voices
    Computer Science · #cs.LO #cs.AI
17. 130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?
    2026/01/06 by Josef Urban · 6 voices · 2 citations
    #cs.LO #cs.AI #cs.SC
18. High schoolers excel at Oxford quantum course using pictorial mathematics
    2025/11/28 by Bob Coecke, Aleks Kissinger, Coecke, Bob +27 · 5 voices
    #physics.ed-ph #cs.LO #math.CT #quant-ph
19. Determination of the fifth Busy Beaver value
    2025/09/15 by The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs +33 · 20 voices · 2 citations
    #cs.LO #cs.FL #math.LO
20. State Algebra for Propositional Logic
    2025/09/12 by Dmitry Lesnik, Lesnik, Dmitry, Tobias Schäfer +1 · 1 voice
    #cs.AI #cs.LO
21. SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs
    2025/08/31 by Yanxiao Zhao, Yaqian Li, Zhao, Yanxiao +15 · 1 citation
    #cs.AI #cs.LG #cs.LO
22. Why Cannot Large Language Models Ever Make True Correct Reasoning?
    2025/08/14 by Jingde Cheng, Cheng, Jingde · 5 voices
    #cs.AI #cs.LO
23. Quantum Circuits Are Just a Phase
    2025/07/15 by Chris Heunen, Heunen, Chris, Louis Lemonnier +6 · 1 voice · 2 citations
    Computer Science · Physics and Astronomy · #Quantum Computing Algorithms and Architecture #cs.LO #cs.PL #quant-ph
24. Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks
    2025/05/26 by Debargha Ganguly, Ganguly, Debargha, Vikash Singh +18 · 4 voices · 3 citations
    Computer Science · #Multi-Agent Systems and Negotiation #cs.AI #cs.CL #cs.LO #cs.SE
25. Automated Verification of Monotonic Data Structure Traversals in C
    2025/05/24 by Matthew Sotoudeh, Sotoudeh, Matthew · 2 voices
    #cs.PL #cs.LO
26. Verified Purely Functional Catenable Real-Time Deques
    2025/05/12 by Jules Viennot, Arthur Wendling, Viennot, Jules +5 · 1 voice
    Computer Science · #Data Structures and Algorithms (cs.DS) #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Programming Languages (cs.PL) #cs.DS #cs.LO #cs.PL
27. Empirical Measures and Strong Laws of Large Numbers in Categorical Probability
    2025/03/27 by Tobias Fritz, Tomáš Gonda, Fritz, Tobias +7 · 1 voice · 3 citations
    #math.PR #cs.LO #math.CT #math.ST
28. Substructural Parametricity
    2025/03/05 by C. B. Aberlé, Aberlé, C. B., Chris Martens +3 · 1 voice · 1 citation
    Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL) #cs.LO #cs.PL
29. Programming Really Is Simple Mathematics
    2025/02/24 by Bertrand Meyer, Meyer, Bertrand, Reto Weber +1 · 1 voice
    Computer Science · #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #Software Engineering (cs.SE) #cs.LO #cs.PL #cs.SE
30. Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
    2025/02/08 by Quinn Dougherty, Dougherty, Quinn, Ronak Mehta +1 · 2 voices · 4 citations
    Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Machine Learning (cs.LG) #Software Engineering (cs.SE) #cs.AI #cs.LG #cs.LO #cs.SE

more