Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!

Administered by:

Server stats:

2.9K
active users

mathstodon.xyz: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#itp

16 posts6 participants0 posts today
José A. Alonso<p>Simplified and verified: A second look at a proof-producing union-find algorithm. ~ Lukas Stevens, Rebecca Ghidini. <a href="https://arxiv.org/abs/2504.10246" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="">arxiv.org/abs/2504.10246</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a></p>
José A. Alonso<p>Proof terms for term rewriting (in Isabelle/HOL). ~ Christina Kirk. <a href="https://www.isa-afp.org/entries/Proof_Terms_Term_Rewriting.html" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">isa-afp.org/entries/Proof_Term</span><span class="invisible">s_Term_Rewriting.html</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a></p>
José A. Alonso<p>First-order rewriting (in Isabelle/HOL). ~ René Thiemann et als. <a href="https://www.isa-afp.org/entries/First_Order_Rewriting.html" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">isa-afp.org/entries/First_Orde</span><span class="invisible">r_Rewriting.html</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a></p>
José A. Alonso<p>The Kolmogorov-Chentsov theorem (in Isabelle/HOL). ~ Christian Pardillo-Laursen, Simon Foster. <a href="https://www.isa-afp.org/entries/Kolmogorov_Chentsov.html" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">isa-afp.org/entries/Kolmogorov</span><span class="invisible">_Chentsov.html</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a></p>
José A. Alonso<p>Readings shared April 13, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/13-readings_shared_04-13-25" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/04/13-readings_shared_04-13-25</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/ATP" class="mention hashtag" rel="tag">#<span>ATP</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Mace4" class="mention hashtag" rel="tag">#<span>Mace4</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Prover9" class="mention hashtag" rel="tag">#<span>Prover9</span></a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="tag">#<span>SetTheory</span></a></p>
José A. Alonso<p>Efficient 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" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="">arxiv.org/abs/2504.07732</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#<span>Coq</span></a></p>
José A. Alonso<p>Completeness 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" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">isa-afp.org/entries/Completene</span><span class="invisible">ss_Decreasing_Diagrams_for_N1.html</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="tag">#<span>SetTheory</span></a></p>
José A. Alonso<p>Readings shared April 11, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/11-readings_shared_04-11-25" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/04/11-readings_shared_04-11-25</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="tag">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Hakell" class="mention hashtag" rel="tag">#<span>Hakell</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="tag">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="tag">#<span>SetTheory</span></a></p>
José A. Alonso<p>A 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" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">preprints.org/manuscript/20250</span><span class="invisible">4.0684/v1</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="tag">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="tag">#<span>SetTheory</span></a></p>
José A. Alonso<p>Code generation via meta-programming in dependently typed proof assistants. ~ Mathis Bouverot-Dupuis, Yannick Forster. <a href="https://hal.science/hal-05024207/document" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">hal.science/hal-05024207/docum</span><span class="invisible">ent</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="tag">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="tag">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a></p>
José A. Alonso<p>Readings shared April 10, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/10-readings_shared_04-10-25" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/04/10-readings_shared_04-10-25</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/ATP" class="mention hashtag" rel="tag">#<span>ATP</span></a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="tag">#<span>CommonLisp</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="tag">#<span>Programming</span></a> <a href="https://mathstodon.xyz/tags/Reasoning" class="mention hashtag" rel="tag">#<span>Reasoning</span></a></p>
José A. Alonso<p>Leanabell-prover: Posttraining scaling in formal reasoning. ~ Jingyuan Zhang et als. <a href="https://arxiv.org/abs/2504.06122" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="">arxiv.org/abs/2504.06122</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a></p>
José A. Alonso<p>Canonical for automated theorem proving in Lean. ~ Chase Norman, Jeremy Avigad. <a href="https://arxiv.org/abs/2504.06239" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="">arxiv.org/abs/2504.06239</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a></p>
José A. Alonso<p>Reasoning about AI’s reasoning. ~ Höjer Key. <a href="https://www.researchgate.net/publication/390527852_Reasoning_about_AI&#39;s_reasoning" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">researchgate.net/publication/3</span><span class="invisible">90527852_Reasoning_about_AI&#39;s_reasoning</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/ATP" class="mention hashtag" rel="tag">#<span>ATP</span></a></p>
José A. Alonso<p>Lemmanaid: Neuro-symbolic lemma conjecturing. ~ Yousef Alhessi et als. <a href="https://arxiv.org/abs/2504.04942" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="">arxiv.org/abs/2504.04942</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a></p>
José A. Alonso<p>Formalization of gyrovector spaces as models of hyperbolic geometry and special relativity (in Isabelle/HOL). ~ Filip Marić, Jelena Markovic. <a href="https://www.isa-afp.org/entries/GyrovectorSpaces.html" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">isa-afp.org/entries/Gyrovector</span><span class="invisible">Spaces.html</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a></p>
José A. Alonso<p>Readings shared April 8, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/08-readings_shared_04-08-25" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/04/08-readings_shared_04-08-25</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="tag">#<span>LogicProgramming</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="tag">#<span>Prolog</span></a></p>
José A. Alonso<p>Training making math proofs using Lean 4. ~ Krillof. <a href="https://github.com/Krillof/Lean4_math_training" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">github.com/Krillof/Lean4_math_</span><span class="invisible">training</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a></p>
José A. Alonso<p>Course Cs2120f24: Discrete mathematics and theory in Lean 4. ~ Kevin Sullivan. <a href="https://github.com/kevinsullivan/cs2120f24" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">github.com/kevinsullivan/cs212</span><span class="invisible">0f24</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a></p>
José A. Alonso<p>DMTL4: Discrete mathematics and theory in Lean 4. ~ Kevin Sullivan. <a href="https://github.com/kevinsullivan/dmtl4" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="">github.com/kevinsullivan/dmtl4</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a></p>
SearchLive feeds
About