Readings shared June 27, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/28-readings_shared_06-27-25 #AI #AI4Math #Autoformalization #CategoryTheory #CompSci #ITP #LLMs #LeanProver #Math #Mizar

LOGICPO: Efficient translation of NL-based logical problems to FOL using LLMs and preference optimization. ~ Koushik Viswanadha, Deepanway Ghosal, Somak Aditay. https://arxiv.org/abs/2506.18383v1 #LLMs #Math #Autoformalization

Readings shared June 13, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/14-readings_shared_06-13-25 #AI #AIforMath #Autoformalization #CoqProver #HOL_Light #ITP #IsabelleHOL #LLMs #LeanProver #Logic #MLLMs #Math #Rocq

The abc conjecture almost always — autoformalized. ~ Jesse Michael Han et als. https://github.com/morph-labs/lean-abc-true-almost-always #Autoformalization #AIforMath #ITP #LeanProver

Trinity: an autoformalization system for verified superintelligence. https://www.morph.so/blog/trinity #Autoformalization #AIforMath #ITP #LeanProver

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

FormalMATH: Benchmarking formal mathematical reasoning of large language models. ~ Zhouliang Yu et als. https://arxiv.org/abs/2505.02735 #LLMs #Autoformalization #Math #ITP #LeanProver

Readings shared February 21, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/21-readings_shared_02-21-25 #AI #Autoformalization #Coq #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LeanProver #Math #OCaml #Rocq

Diverse inference and verification for advanced reasoning. ~ Iddo Drori et als. https://arxiv.org/abs/2502.09955 #LLMs #ITP #LeanProver #Autoformalization

Formalizing complex mathematical statements with LLMs: A study on mathematical definitions. ~ Lan Zhang, Marco Valentino, Andre Freitas. https://arxiv.org/abs/2502.12065 #LLMs #Math #Autoformalization #ITP #IsabelleHOL

Readings shared February 14, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/14-readings_shared_02-14-25 #Autoformalization #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs

Language models for verifiable mathematical automation (Interaction, integration, and autoformalization). ~ Qiaochu Jiang. https://www.repository.cam.ac.uk/items/6ccd12ea-25c5-4950-9dab-0f8e6fb691fd #ITP #IsabelleHOL #LLMs #Autoformalization

Readings shared February 13, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/13-readings_shared_02-13-25 #AI #Autoformalization #Coq #ITP #IsabelleHOL #LLMs #LeanProver #LogicProgramming #Math #Programming #Prolog #Rocq

Improving autoformalization using type checking. ~ Auguste Poiroux, Gail Weiss, Viktor Kunčak, Antoine Bosselut. https://arxiv.org/abs/2406.07222 #Autoformalization #LLMs #ITP #LeanProver #Math

ATLAS: Autoformalizing theorems through lifting, augmentation, and synthesis of data. ~ Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao, Tao Luo. https://arxiv.org/abs/2502.05567 #LLMs #ITP #LeanProver #Math #Autoformalization

Readings shared December 23, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/23-readings_shared_12-23-24 #AI #Math #Reasoning #ITP #Coq #IsabelleHOL #LeanProver #Autoformalization #Programming #JuliaLang #Python #MachineLearning #Golog #LogicProgramming

Formal mathematical reasoning: A new frontier in AI. ~ Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, Dawn Song. https://arxiv.org/abs/2412.16075 #AI #Math #Reasoning #ITP #Coq #IsabelleHOL #LeanProver #Autoformalization

Readings shared November 2, 2024. https://jaalonso.github.io/vestigium/posts/2024/11/02-readings_shared_11-02-24 #ITP #LeanProver #IsabelleHOL #Coq #Math #SetTheory #CategoryTheory #AI #LLMs #Autoformalization

The future of Mathematics in a world of machines. ~ Simone Severini. https://www.linkedin.com/pulse/future-mathematics-world-machines-simone-severini-v6odc/ #Math #ITP #LeanProver #AI #LLMs #Autoformalization

Readings shared November 1, 2024. https://jaalonso.github.io/vestigium/posts/2024/11/01-readings_shared_11-01-24 #ITP #Lean4 #IsabelleHOL #Coq #Logic #Math #Haskell #FunctionalProgramming #Autoformalization #LLMs