Lingolol

José A. AlonsoReadings shared April 4, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/04-readings_shared_04-04-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/04/04-readings_shared_04-04-25</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Maxima" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Maxima</a>

José A. AlonsoLearning Lean in the age of Artificial Intelligence. ~ Adolfo Neto. <a href="https://youtu.be/plpPffJOKu8" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://youtu.be/plpPffJOKu8</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a>

José A. AlonsoReadings shared April 3, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/03-readings_shared_04-03-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/04/03-readings_shared_04-03-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AlphaProof</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a>

José A. AlonsoLeanSolver: Solving theorems through large language models and search. ~ Avi Luciano Halevy <a href="https://repository.tudelft.nl/file/File_a98b6c93-4017-42c5-bb8f-df68da0d7034" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://repository.tudelft.nl/file/File_a98b6c93-4017-42c5-bb8f-df68da0d7034</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a>

José A. AlonsoMorley's theorem (in Isabelle/HOL). ~ Benjamin Puyobro. <a href="https://www.isa-afp.org/entries/Morley_Theorem.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.isa-afp.org/entries/Morley_Theorem.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a>

José A. AlonsoReadings shared April 2, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/02-readings_shared_04-02-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/04/02-readings_shared_04-02-25</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#HOL4</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LogicProgramming</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Mathlib" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Mathlib</a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Prolog</a>

José A. AlonsoCurso: Demostración asistida por ordenador (2010-11). <a href="https://jaalonso.github.io/cursos/DAO2011" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/cursos/DAO2011</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/L%C3%B3gica" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Lógica</a>

José A. AlonsoBasic probability in Mathlib. ~ Rémy Degenne. <a href="https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Mathlib" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Mathlib</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a>

José A. AlonsoGOL in GOL in HOL: Verified circuits in Conway's game of life. ~ Magnus O. Myreen, Mario Carneiro. <a href="https://arxiv.org/abs/2504.00263" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://arxiv.org/abs/2504.00263</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#HOL4</a>

José A. AlonsoReadings shared April 1, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/01-readings_shared_04-01-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/04/01-readings_shared_04-01-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LogicProgramming</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Prolog</a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#SMT</a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Z3</a>

José A. AlonsoIntroducción a la demostración asistida por ordenador con Isabelle/HOL (versión de 7 de agosto de 2010). <a href="https://web.archive.org/web/https://www.cs.us.es/~jalonso/cursos/m-ra-10/temas/IDAO.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://web.archive.org/web/https://www.cs.us.es/~jalonso/cursos/m-ra-10/temas/IDAO.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a>

José A. AlonsoCurso "Razonamiento automático (2010-11)". <a href="https://jaalonso.github.io/cursos/m-ra-10" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/cursos/m-ra-10</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a>

José A. AlonsoSTP: Self-play LLM theorem provers with iterative conjecturing and proving. ~ Kefan Dong, Tengyu Ma. <a href="https://arxiv.org/abs/2502.00212" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://arxiv.org/abs/2502.00212</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a>

José A. AlonsoReadings shared March 31, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/31-readings_shared_03-31-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/03/31-readings_shared_03-31-25</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#CompSci</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a>

José A. AlonsoFormally verifying a transformation from MLTL formulas to regular expressions. ~ Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier. <a href="https://research.temporallogic.org/papers/WKR25.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://research.temporallogic.org/papers/WKR25.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a>

José A. AlonsoReadings shared March 30, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/30-readings_shared_03-30-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/03/30-readings_shared_03-30-25</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Maxima" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Maxima</a>

José A. AlonsoIntroducing clean, a formal verification DSL for zk circuits in Lean4. ~ Giorgio Dell'Immagine. <a href="https://blog.zksecurity.xyz/posts/clean/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://blog.zksecurity.xyz/posts/clean/</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a>

José A. AlonsoTowards mechanized verification of Verilog equivalence checking. ~ Michalis Pardalos, Laura Pozzi, John Wickerson. <a href="https://johnwickerson.github.io/papers/vera_LATTE25.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://johnwickerson.github.io/papers/vera_LATTE25.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Coq</a>

José A. AlonsoReadings shared March 29, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/29-readings_shared_03-29-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/03/29-readings_shared_03-29-25</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a>

José A. AlonsoLean formalization of generalization error bound by Rademacher complexity. ~ Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda. <a href="https://arxiv.org/abs/2503.19605" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://arxiv.org/abs/2503.19605</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a>

Recent searches

Search options

Administered by:

Server stats:

#ITP