Mastodon

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

José A. AlonsoNon-circular trigonometric proofs of the pythagorean theorem in Lean4: A comparison. ~ Paul Pajo. <a href="https://www.researchgate.net/publication/390875819_Non-Circular_Trigonometric_Proofs_of_the_Pythagorean_Theorem_in_Lean4_A_Comparison" rel="nofollow noopener" translate="no" target="_blank">https://www.researchgate.net/publication/390875819_Non-Circular_Trigonometric_Proofs_of_the_Pythagorean_Theorem_in_Lean4_A_Comparison</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoEnhancing AI trustworthiness through automated reasoning: A novel method for explaining deep learning and LLM reasoning. ~ Julia Connolly, Oliver Stanton, Sarah Veronica, Liam Whitmore. <a href="https://www.researchgate.net/publication/390844466_Enhancing_AI_Trustworthiness_Through_Automated_Reasoning_A_Novel_Method_for_Explaining_Deep_Learning_and_LLM_Reasoning" rel="nofollow noopener" translate="no" target="_blank">https://www.researchgate.net/publication/390844466_Enhancing_AI_Trustworthiness_Through_Automated_Reasoning_A_Novel_Method_for_Explaining_Deep_Learning_and_LLM_Reasoning</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/Reasoning" class="mention hashtag" rel="nofollow noopener" target="_blank">#Reasoning</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a>

José A. AlonsoA formalisation of Aristotle’s assertoric syllogistic in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki, Karol Wapniarski. <a href="https://link.springer.com/article/10.1007/s11245-025-10184-6" rel="nofollow noopener" translate="no" target="_blank">https://link.springer.com/article/10.1007/s11245-025-10184-6</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a>

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

José A. AlonsoNeural theorem proving tutorial. ~ Sean Welleck. <a href="https://github.com/wellecks/ntptutorial" rel="nofollow noopener" translate="no" target="_blank">https://github.com/wellecks/ntptutorial</a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener" target="_blank">#MachineLearning</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a>

José A. AlonsoKnuckledragger: A low barrier proof assistant. ~ Philip Zucker. <a href="https://github.com/philzook58/knuckledragger" rel="nofollow noopener" translate="no" target="_blank">https://github.com/philzook58/knuckledragger</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#SMT</a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#Z3</a> <a href="https://mathstodon.xyz/tags/Python" class="mention hashtag" rel="nofollow noopener" target="_blank">#Python</a>

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

José A. AlonsoA readable and computable formalization of the Streamlet consensus protocol. ~ Mauro Jaskelioff, Orestis Melkonian, James Chapman. <a href="https://omelkonian.github.io/data/publications/formal-streamlet.pdf" rel="nofollow noopener" translate="no" target="_blank">https://omelkonian.github.io/data/publications/formal-streamlet.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a>

José A. AlonsoFormalization of Fraïssé limits in Lean. ~ Gabin Kolly. <a href="https://www.math.uni-bonn.de/people/phierony/Kolly.pdf" rel="nofollow noopener" translate="no" target="_blank">https://www.math.uni-bonn.de/people/phierony/Kolly.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

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

José A. AlonsoSimplified and verified: A second look at a proof-producing union-find algorithm. ~ Lukas Stevens, Rebecca Ghidini. <a href="https://arxiv.org/abs/2504.10246" rel="nofollow noopener" translate="no" target="_blank">https://arxiv.org/abs/2504.10246</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a>

José A. AlonsoProof terms for term rewriting (in Isabelle/HOL). ~ Christina Kirk. <a href="https://www.isa-afp.org/entries/Proof_Terms_Term_Rewriting.html" rel="nofollow noopener" translate="no" target="_blank">https://www.isa-afp.org/entries/Proof_Terms_Term_Rewriting.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a>

José A. AlonsoFirst-order rewriting (in Isabelle/HOL). ~ René Thiemann et als. <a href="https://www.isa-afp.org/entries/First_Order_Rewriting.html" rel="nofollow noopener" translate="no" target="_blank">https://www.isa-afp.org/entries/First_Order_Rewriting.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a>

José A. AlonsoThe Kolmogorov-Chentsov theorem (in Isabelle/HOL). ~ Christian Pardillo-Laursen, Simon Foster. <a href="https://www.isa-afp.org/entries/Kolmogorov_Chentsov.html" rel="nofollow noopener" translate="no" target="_blank">https://www.isa-afp.org/entries/Kolmogorov_Chentsov.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

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

José A. AlonsoEfficient formal verification of quantum error correcting programs. ~ Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, Mingsheng Ying. <a href="https://arxiv.org/abs/2504.07732" rel="nofollow noopener" translate="no" target="_blank">https://arxiv.org/abs/2504.07732</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a>

José A. AlonsoCompleteness of decreasing diagrams for the least uncountable cardinality (in Isabelle/HOL). ~ Ievgen Ivanov. <a href="https://www.isa-afp.org/entries/Completeness_Decreasing_Diagrams_for_N1.html" rel="nofollow noopener" translate="no" target="_blank">https://www.isa-afp.org/entries/Completeness_Decreasing_Diagrams_for_N1.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#SetTheory</a>

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

José A. AlonsoA comparative review of ZFC, NBG, and MK axiom systems: Theoretical foundations and formalization in Coq. ~ Si Chen, Wensheng Yu. <a href="https://www.preprints.org/manuscript/202504.0684/v1" rel="nofollow noopener" translate="no" target="_blank">https://www.preprints.org/manuscript/202504.0684/v1</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#SetTheory</a>

Recent searches

Search options

Administered by:

Server stats:

#itp