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>
eupolicy.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
This Mastodon server is a friendly and respectful discussion space for people working in areas related to EU policy. When you request to create an account, please tell us something about you.
Administered by:
Server stats:
202active users
eupolicy.social: About · Profiles directory · Privacy policy
Mastodon: About · Get the app · Keyboard shortcuts · View source code · v4.4.1
#leanprover
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>Readings shared July 29, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/30-readings_shared_07-29-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/07/30-readings_shared_07-29-25</span></a> <a href="https://mathstodon.xyz/tags/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CoqProver</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalVerification</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/IMO" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IMO</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/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/ProofAssistant" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ProofAssistant</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/Rust" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rust</span></a></p>
José A. Alonso<p>Symbolic world models in Lean 4 for reinforcement learning. ~ Matěj Kripner. <a href="https://openreview.net/forum?id=CBFAMnax09" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">openreview.net/forum?id=CBFAMn</span><span class="invisible">ax09</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/MachineLearning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MachineLearning</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>
Lean<p>📣 We're excited to share the new lean-lang.org!</p><p>Relaunching our website was a key deliverable in our Year 2 roadmap to provide "improved navigation and access to valuable content, resources, and tools." We hope you like it!</p><p><a href="https://functional.cafe/tags/LeanLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanLang</span></a> <a href="https://functional.cafe/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a></p>
José A. Alonso<p>Readings shared July 4, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/05-readings_shared_07-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/07/05-readings_shared_07-04-25</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</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/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/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/Rust" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rust</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>ProofAug: Efficient neural theorem proving via fine-grained proof structure analysis. ~ Haoxiong Liu et als. <a href="https://openreview.net/pdf?id=GCjsjnl8yA" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">openreview.net/pdf?id=GCjsjnl8</span><span class="invisible">yA</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/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></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>
Lean<p>We are deeply grateful to ACM SIGPLAN for recognizing <a href="https://functional.cafe/tags/LeanLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanLang</span></a> with the Programming Languages Software Award 2025 at <a href="https://functional.cafe/tags/PLDI2025" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>PLDI2025</span></a>.</p><p>The citation states: "The Lean theorem prover is a remarkable software artifact. Grounded on strong theoretical and engineering foundations, Lean has had and continues to have a broad impact on industrial practice and scientific research."</p><p>Unquestionably, this recognition belongs to the community as much as it does the original authors - especially to the many mathematicians and contributors who have helped to build Mathlib to over 1.8M lines of code. As Soonho Kong said on accepting the award: "This award goes to the actual Lean community and all the people who love Lean and using Lean." </p><p>Thank you to everyone who has contributed to making formal mathematics more accessible and reliable!</p><p><a href="https://functional.cafe/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://functional.cafe/tags/FormalMathmatics" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalMathmatics</span></a></p>
Andrej Bauer<p>I taught a class on formalized mathematics in Lean. Today two projects were handed in, and both of them are quite impressive.</p><p>In the first project, Luka Opravš formalized Polya's enumeration theorem, and then proceeded to also implement and formally verify an efficient algorithmic version.</p><p>It takes Lean only a moment to formally compute that there are</p><p>3734642804542694673304928339684903440360290548300415176063232044682349196517954782034451010203315482100413928177255823637569999967383129500169880004095283194405966596476413742304023127572767115899</p><p>distinct colorings of a necklace with 99 beads and 99 colors. See Luka's blueprint for details (and give his repository a star while you're at it).</p><p><a href="https://github.com/Luka-O/polya-enumeration-theorem" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">github.com/Luka-O/polya-enumer</span><span class="invisible">ation-theorem</span></a></p><p><a href="https://mathstodon.xyz/tags/Leanprover" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Leanprover</span></a></p>
José A. Alonso<p>A complete formalization of Fermat's Last Theorem for regular primes in Lean. ~ Alex Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi, Ruben van De Velde, Andrew Yang. <a href="https://arxiv.org/abs/2410.01466" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2410.01466</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 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>Common Lean pitfalls. ~ Niels Voss. <a href="https://github.com/nielsvoss/lean-pitfalls" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">github.com/nielsvoss/lean-pitf</span><span class="invisible">alls</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>Sequencelib: A platform for formalizing in Lean 4 sequences from "The On-Line Encyclopedia of Integer Sequences" (OEIS). ~ Walter Moreira, Joe Stubbs. <a href="https://provables.github.io/sequencelib/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">provables.github.io/sequenceli</span><span class="invisible">b/</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>
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