Readings shared June 3, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/03-readings_shared_06-03-25 #AI #ATP #Emacs #ITP #IsabelleHOL #LeanProver #Logic #Math #SAT_Solvers

Readings shared May 20, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/20-readings_shared_05-20-25 #Agda #Emacs #FunctionalProgramming #Haskell #HoTT #ITP #LeanProver #Logic #Math #OrgMode #Python #Rust #SAT_solvers #TypeTheory

Symbolic sets for proving bounds on Rado numbers. ~ Tanbir Ahmed, Lamina Zaman, Curtis Bright. https://arxiv.org/abs/2505.12085# #SAT_solvers #Python #Math

Readings shared May 8, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/08-readings_shared_05-08-25 #ATP #Autoformalization #FunctionalProgramming #Haskell #ITP #LLMs #LeanProver #Math #Programming #SAT_solvers #Z3

SAT-solving the poset cover problem. ~ Chih-Cheng Rex Yuan, Bow-Yaw Wang. https://arxiv.org/abs/2505.04013 #ATP #SAT_solvers #Z3

Can Transformers reason logically? A study in SAT solving. ~ Leyan Pan, Vijay Ganesh, Jacob Abernethy, Chris Esposo, Wenke Lee. https://arxiv.org/abs/2410.07432 #LLMs #Reasoning #SAT_Solvers

Readings shared November 13, 2024. https://jaalonso.github.io/vestigium/posts/2024/11/13-readings_shared_11-13-24 #ITP #Lean4 #Math #Physics #ATP #SAT_Solvers

How to discover short, shorter, and the shortest proofs of unsatisfiability: A branch-and-bound approach for resolution proof length minimization. ~ Konstantin Sidorov, Koos van der Linden, Gonçalo Homem de Almeida Correia, Mathijs de Weerdt, Emir Demirović. https://arxiv.org/abs/2411.07955 #ATP #SAT_Solvers