José A. Alonso<p>Simple groups in Lean (Video). ~ Antoine Chambert-Loir. <a href="https://youtu.be/yy66Dgod2gE" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/yy66Dgod2gE</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/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>
toad.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
Mastodon server operated by David Troy, a tech pioneer and investigative journalist addressing threats to democracy. Thoughtful participation and discussion welcome.
Administered by:
Server stats:
273active users
toad.social: About · Profiles directory · Privacy policy
Mastodon: About · Get the app · Keyboard shortcuts · View source code · v4.4.1
#ITP
0 posts · 0 participants · 0 posts today
José A. Alonso<p>A crash course on type theory (Video). ~ Antoine Chambert-Loir. <a href="https://youtu.be/7Uux3Vuwnhg" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/7Uux3Vuwnhg</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/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TypeTheory</span></a></p>
José A. Alonso<p>A crash course on type theory. ~ Antoine Chambert-Loir. <a href="https://webusers.imj-prg.fr/~antoine.chambert-loir/exposes/accitt.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">webusers.imj-prg.fr/~antoine.c</span><span class="invisible">hambert-loir/exposes/accitt.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/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TypeTheory</span></a></p>
José A. Alonso<p>Doing elementary number theory in Lean (Video 2). ~ Antoine Chambert-Loir <a href="https://youtu.be/2w-PX3GhYXg" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/2w-PX3GhYXg</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/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>Scaling mathematical reasoning through data, tools, and generative selection. ~ Ivan Moshkov et als. <a href="https://openreview.net/forum?id=OM7ZN0PmSS" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">openreview.net/forum?id=OM7ZN0</span><span class="invisible">PmSS</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/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/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. <a href="https://arxiv.org/abs/2503.00959" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2503.00959</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/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>Dyck language (in Isabelle/HOL). ~ Tobias Nipkow, Moritz Roos. <a href="https://www.isa-afp.org/entries/Dyck_Language.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">isa-afp.org/entries/Dyck_Langu</span><span class="invisible">age.html</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></p>
José A. Alonso<p>Readings shared June 14, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/15-readings_shared_06-14-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/06/15-readings_shared_06-14-25</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/Emacs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Emacs</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/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/Maxima" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Maxima</span></a></p>
José A. Alonso<p>Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. <a href="https://arxiv.org/abs/2503.00959" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2503.00959</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/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>Lean meta-theory: The proofs behind the proofs. ~ Mario Carneiro. <a href="https://www.youtube.com/live/YtbfIjgzNDI" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="">youtube.com/live/YtbfIjgzNDI</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/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a></p>
José A. Alonso<p>Formalizing the divided power envelope in Lean. ~ María Inés de Frutos Fernández. <a href="https://www.youtube.com/live/R2t9ZRWiWEk" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="">youtube.com/live/R2t9ZRWiWEk</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/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 June 8, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/08-readings_shared_06-08-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/06/08-readings_shared_06-08-25</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/Algorithms" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Algorithms</span></a> <a href="https://mathstodon.xyz/tags/CAS" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CAS</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/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</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/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/Maxima" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Maxima</span></a> <a href="https://mathstodon.xyz/tags/Reasoning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Reasoning</span></a></p>
José A. Alonso<p>Functional programming in Lean. ~ David Thrane Christiansen. <a href="https://lean-lang.org/functional_programming_in_lean/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">lean-lang.org/functional_progr</span><span class="invisible">amming_in_lean/</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/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a></p>
José A. Alonso<p>Construire des preuves mathématiques. ~ Thierry Coquand, William Rowe-Pirra. <a href="https://interstices.info/construire-des-preuves-mathematiques/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">interstices.info/construire-de</span><span class="invisible">s-preuves-mathematiques/</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></p>
José A. Alonso<p>A formalization of elementary linear algebra: Part I. ~ David M. Russinoff. <a href="https://www.russinoff.com/papers/linear1.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">russinoff.com/papers/linear1.p</span><span class="invisible">df</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/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ACL2</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>Will computers prove theorems? ~ Kevin Buzzard. <a href="https://youtu.be/LylJBfvVzyw" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/LylJBfvVzyw</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/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>A Lean proof of Fermat’s Last Theorem. ~ Kevin Buzzard, Richard Taylor. <a href="https://imperialcollegelondon.github.io/FLT/blueprint.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">imperialcollegelondon.github.i</span><span class="invisible">o/FLT/blueprint.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/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>Formalizing a proof in Lean using Claude and o4. ~ Terence Tao. <a href="https://youtu.be/zZr54G7ec7A" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/zZr54G7ec7A</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/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>Will computers prove theorems? ~ Kevin Buzzard. <a href="https://podcasts.ox.ac.uk/will-computers-prove-theorems" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">podcasts.ox.ac.uk/will-compute</span><span class="invisible">rs-prove-theorems</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/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</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" rel="nofollow noopener" translate="no" target="_blank"><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="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></p>
TrendingLive feeds
Mastodon is the best way to keep up with what's happening.
Follow anyone across the fediverse and see it all in chronological order. No algorithms, ads, or clickbait in sight.
Create accountLoginDrag & drop to upload