101010.pl is one of the many independent Mastodon servers you can use to participate in the fediverse.
101010.pl czyli najstarszy polski serwer Mastodon. Posiadamy wpisy do 2048 znaków.

Server stats:

508
active users

#hol_light

0 posts0 participants0 posts today
José A. Alonso<p>Readings shared March 23, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/23-readings_shared_03-23-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/03/23-readings_shared_03-23-25</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Mizar</span></a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SetTheory</span></a></p>
José A. Alonso<p>A review on mechanical proving and formalization of mathematical theorems. ~ Si Chen, Wensheng Yu, Guowei Dou, Qimeng Zhang. <a href="https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=10930874" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">ieeexplore.ieee.org/stamp/stam</span><span class="invisible">p.jsp?arnumber=10930874</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Mizar</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Readings shared January 26, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/26-readings_shared_01-26-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/01/26-readings_shared_01-26-25</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Formalization of partial differential equations using HOL theorem proving. ~ Elif Deniz. <a href="https://hvg.ece.concordia.ca/Publications/Thesis/Elif-PhD-Thesis.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">hvg.ece.concordia.ca/Publicati</span><span class="invisible">ons/Thesis/Elif-PhD-Thesis.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Readings shared January 4, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/04-readings_shared_01-04-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/01/04-readings_shared_01-04-25</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Mizar</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/Python" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Python</span></a></p>
José A. Alonso<p>Growing HOLMS, a HOL Light library for modal systems. ~ Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini. <a href="https://overlay.uniud.it/workshop/2024/papers/paper5.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">overlay.uniud.it/workshop/2024</span><span class="invisible">/papers/paper5.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a></p>
José A. Alonso<p>Readings shared September 28, 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/09/28-readings_shared_09-28-24" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2024/09/28-readings_shared_09-28-24</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Formal verification of coupled transmission lines using theorem proving. ~ Elif Deniz, Adnan Rashid &amp; Sofiène Tahar. <a href="https://hvg.ece.concordia.ca/projects/fvps/pde/Formal_Verification_of_Coupled_Transmission_Lines.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">hvg.ece.concordia.ca/projects/</span><span class="invisible">fvps/pde/Formal_Verification_of_Coupled_Transmission_Lines.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a></p>
José A. Alonso<p>Readings shared September 14, 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/09/14-readings_shared_09-14-24" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2024/09/14-readings_shared_09-14-24</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/LambdaCalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LambdaCalculus</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a></p>
José A. Alonso<p>Better-performing “25519” elliptic-curve cryptography (Automated reasoning and optimizations specific to CPU microarchitectures improve both performance and assurance of correct implementation). ~ Torben Hansen, John Harrison. <a href="https://www.amazon.science/blog/better-performing-25519-elliptic-curve-cryptography" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">amazon.science/blog/better-per</span><span class="invisible">forming-25519-elliptic-curve-cryptography</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a></p>
José A. Alonso<p>Lecturas compartidas el 25 de junio de 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/06/26-lecturas_compartidas_el_25-jun-24" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2024/06/26-lecturas_compartidas_el_25-jun-24</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/HOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/Metamath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Metamath</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/Python" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Python</span></a> <a href="https://mathstodon.xyz/tags/Algorithms" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Algorithms</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MachineLearning</span></a></p>
José A. Alonso<p>Even more on HOL Light (3). ~ Freek Wiedijk. <a href="https://youtu.be/R-3kPIHB2RA" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/R-3kPIHB2RA</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a></p>
José A. Alonso<p>More on HOL Light (2). ~ Freek Wiedijk. <a href="https://youtu.be/ux96swHX-6s" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/ux96swHX-6s</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a></p>
José A. Alonso<p>Lecturas compartidas el 6 de junio de 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/06/07-lecturas_compartidas_el_06-jun-24" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2024/06/07-lecturas_compartidas_el_06-jun-24</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>The HOL Light library of formalized mathematics. ~ Marco Maggesi. <a href="https://europroofnet.github.io/_pages/WG4/Sep22/maggesi.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">europroofnet.github.io/_pages/</span><span class="invisible">WG4/Sep22/maggesi.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Lecturas compartidas el 30 de mayo de 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/05/31-lecturas_compartidas_el_30-may-24" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2024/05/31-lecturas_compartidas_el_30-may-24</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Theorema" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Theorema</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/ATP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ATP</span></a> <a href="https://mathstodon.xyz/tags/Prover9" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Prover9</span></a> <a href="https://mathstodon.xyz/tags/Vampire" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Vampire</span></a> <a href="https://mathstodon.xyz/tags/TPTP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TPTP</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LogicProgramming</span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Prolog</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a></p>
José A. Alonso<p>Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. <a href="https://easychair.org/publications/paper/mtFT" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">easychair.org/publications/pap</span><span class="invisible">er/mtFT</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a></p>
José A. Alonso<p>Lecturas compartidas el 11 de mayo de 2024. <a href="https://jalonso.substack.com/lecturas-compartidas-el-11-de-mayo" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jalonso.substack.com/lecturas-</span><span class="invisible">compartidas-el-11-de-mayo</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Metamath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Metamath</span></a> <a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Mizar</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Programming</span></a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CommonLisp</span></a></p>
José A. Alonso<p>Algorithm and abstraction in formal mathematics. ~ Heather Macbeth. <a href="https://arxiv.org/abs/2405.04699" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2405.04699</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Metamath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Metamath</span></a> <a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Mizar</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Lecturas compartidas el 8 de mayo de 2024. <a href="https://jalonso.substack.com/lecturas-compartidas-el-8-de-mayo" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jalonso.substack.com/lecturas-</span><span class="invisible">compartidas-el-8-de-mayo</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL4</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. <a href="https://files.inria.fr/blanqui/lpar24.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">files.inria.fr/blanqui/lpar24.</span><span class="invisible">pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a></p>
José A. Alonso<p>Lecturas compartidas el 28 de abril de 2024. <a href="https://jalonso.substack.com/lecturas-compartidas-el-28-de-abril" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jalonso.substack.com/lecturas-</span><span class="invisible">compartidas-el-28-de-abril</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Formalization of the telegrapher’s equations using higher-order-logic theorem proving. ~ Elif Deniz, Adnan Rashid, Osman Hasan, Sofiène Tahar. <a href="https://www.researchgate.net/profile/Adnan-Rashid-7/publication/379913006_Formalization_of_the_Telegrapher's_Equations_using_Higher-Order-Logic_Theorem_Proving/links/6621a78239e7641c0bd77086/Formalization-of-the-Telegraphers-Equations-using-Higher-Order-Logic-Theorem-Proving.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">researchgate.net/profile/Adnan</span><span class="invisible">-Rashid-7/publication/379913006_Formalization_of_the_Telegrapher's_Equations_using_Higher-Order-Logic_Theorem_Proving/links/6621a78239e7641c0bd77086/Formalization-of-the-Telegraphers-Equations-using-Higher-Order-Logic-Theorem-Proving.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Lecturas compartidas el 16 de abril de 2024. <a href="https://jalonso.substack.com/lecturas-compartidas-el-16-de-abril" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jalonso.substack.com/lecturas-</span><span class="invisible">compartidas-el-16-de-abril</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/Python" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Python</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CompSci</span></a></p>
José A. Alonso<p>Asymptotics for the standard block size in primal lattice attacks: second order, formally verified. ~ Daniel J. Bernstein. <a href="https://cr.yp.to/papers/latticeasymp-20240413.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">cr.yp.to/papers/latticeasymp-2</span><span class="invisible">0240413.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a></p>
José A. Alonso<p>Lecturas compartidas el 18 de marzo de 2024. <a href="https://jalonso.substack.com/lecturas-compartidas-el-18-de-marzo" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jalonso.substack.com/lecturas-</span><span class="invisible">compartidas-el-18-de-marzo</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/ATP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ATP</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MachineLearning</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/ProofAssistants" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ProofAssistants</span></a></p>
José A. Alonso<p>Machine assisted proofs. ~ Terence Tao (<span class="h-card" translate="no"><a href="https://mathstodon.xyz/@tao" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>tao</span></a></span>). <a href="https://terrytao.files.wordpress.com/2024/03/machine-assisted-proof-notices.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">terrytao.files.wordpress.com/2</span><span class="invisible">024/03/machine-assisted-proof-notices.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/ProofAssistants" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ProofAssistants</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MachineLearning</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Machine assisted proofs [Slides]. ~ Terence Tao (<span class="h-card" translate="no"><a href="https://mathstodon.xyz/@tao" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>tao</span></a></span>). <a href="https://terrytao.files.wordpress.com/2024/03/machine-jan-3.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">terrytao.files.wordpress.com/2</span><span class="invisible">024/03/machine-jan-3.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/ProofAssistants" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ProofAssistants</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MachineLearning</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>The formal proof of the Kepler conjecture: a critical retrospective. ~ Thomas Hales. <a href="https://arxiv.org/abs/2402.08032v1" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2402.08032v1</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Mechanising Gödel-Löb provability logic in HOL Light. ~ Marco Maggesi, Cosimo Perini Brogi. <a href="https://arxiv.org/abs/2205.03659" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2205.03659</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a></p>
José A. Alonso<p>HOL Light from the foundations (part 3/3). ~ John Harrison. <a href="https://itp-school-2023.github.io/slides/slides_jrh_part3.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">itp-school-2023.github.io/slid</span><span class="invisible">es/slides_jrh_part3.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a></p>
José A. Alonso<p>HOL Light from the foundations (part 2/3). ~ John Harrison. <a href="https://itp-school-2023.github.io/slides/slides_jrh_part2.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">itp-school-2023.github.io/slid</span><span class="invisible">es/slides_jrh_part2.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a></p>
José A. Alonso<p>Mechanising Gödel–Löb provability logic in HOL Light. ~ Marco Maggesi, Cosimo Perini Brogi. <a href="https://www.researchgate.net/publication/373491652_Mechanising_Godel-Lob_Provability_Logic_in_HOL_Light" rel="nofollow noopener" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">researchgate.net/publication/3</span><span class="invisible">73491652_Mechanising_Godel-Lob_Provability_Logic_in_HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a></p>