'/%3e%3cpath%20d='M50.3943%2022.237V39.5876H43.5185V22.7481C43.5185%2019.2029%2042.0411%2017.3949%2039.036%2017.3949C35.7325%2017.3949%2034.0778%2019.5338%2034.0778%2023.7585V32.9759H27.2434V23.7585C27.2434%2019.5338%2025.5857%2017.3949%2022.2822%2017.3949C19.2949%2017.3949%2017.8027%2019.2029%2017.8027%2022.7481V39.5876H10.9298V22.237C10.9298%2018.6918%2011.835%2015.8754%2013.6453%2013.7877C15.5128%2011.7049%2017.9623%2010.6355%2021.0028%2010.6355C24.522%2010.6355%2027.1813%2011.9885%2028.9542%2014.6917L30.665%2017.5633L32.3788%2014.6917C34.1517%2011.9885%2036.811%2010.6355%2040.3243%2010.6355C43.3619%2010.6355%2045.8114%2011.7049%2047.6847%2013.7877C49.4931%2015.8734%2050.3963%2018.6899%2050.3943%2022.237Z'%20fill='white'/%3e%3cdefs%3e%3clinearGradient%20id='paint0_linear_89_8'%20x1='30.5'%20y1='0'%20x2='30.5'%20y2='65'%20gradientUnits='userSpaceOnUse'%3e%3cstop%20stop-color='%236364FF'/%3e%3cstop%20offset='1'%20stop-color='%23563ACC'/%3e%3c/linearGradient%3e%3c/defs%3e%3c/svg%3e)
José A. Alonso<p>Trinity: an autoformalization system for verified superintelligence. <a href="https://www.morph.so/blog/trinity" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="">morph.so/blog/trinity</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/Autoformalization" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Autoformalization</span></a> <a href="https://mathstodon.xyz/tags/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</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>
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.
Administered by:
Server stats:
516active users
101010.pl: About · Status · Profiles directory · Privacy policy
Mastodon: About · Get the app · Keyboard shortcuts · View source code · v4.4.0-beta.1
#leanprover
32 posts · 7 participants · 7 posts today
José A. Alonso<p>Reseña de «Mathesis: Towards formal theorem proving from natural languages». <a href="https://jaalonso.github.io/vestigium/posts/2025/06/13-resena-de-mathesis-towards-formal-theorem-proving-from-natural-languages/" 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/13-resena-de-mathesis-towards-formal-theorem-proving-from-natural-languages/</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> <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/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/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</span></a></p>
José A. Alonso<p>Mathesis: Towards formal theorem proving from natural languages. ~ Yu Xuejun et als. <a href="https://arxiv.org/abs/2506.07047" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2506.07047</span><span class="invisible"></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> <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/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/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</span></a></p>
José A. Alonso<p>Reseña de «MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems?». <a href="https://jaalonso.github.io/vestigium/posts/2025/06/13-resena-de-matp-bench-can-mllm-be-a-good-automated-theorem-prover-for-multimodal-problems/" 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/13-resena-de-matp-bench-can-mllm-be-a-good-automated-theorem-prover-for-multimodal-problems/</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/MLLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MLLMs</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/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/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CoqProver</span></a> <a href="https://mathstodon.xyz/tags/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</span></a></p>
José A. Alonso<p>MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems? ~ Zhitao He et als. <a href="https://arxiv.org/abs/2506.06034" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2506.06034</span><span class="invisible"></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/MLLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MLLMs</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/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/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CoqProver</span></a> <a href="https://mathstodon.xyz/tags/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</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>Readings shared June 12, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/13-readings_shared_06-12-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/13-readings_shared_06-12-25</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/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CoqProver</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/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/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a></p>
José A. Alonso<p>Lean Copilot: Large language models as copilots for theorem proving in Lean. ~ Peiyang Song, Kaiyu Yang, Anima Anandkumar. <a href="https://neus-2025.github.io/files/papers/paper_33.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">neus-2025.github.io/files/pape</span><span class="invisible">rs/paper_33.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/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</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 11, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/12-readings_shared_06-11-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/12-readings_shared_06-11-25</span></a> <a href="https://mathstodon.xyz/tags/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</span></a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CompSci</span></a> <a href="https://mathstodon.xyz/tags/IA" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IA</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/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/RustLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>RustLang</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/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a></p>
José A. Alonso<p>Reseña de 'LeanTutor: A formally-verified AI tutor for mathematical proofs'. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/11-resena-de-leantutor-a-formally-verified-ai-tutor-for-mathematical-proofs/" 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/11-resena-de-leantutor-a-formally-verified-ai-tutor-for-mathematical-proofs/</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> <a href="https://mathstodon.xyz/tags/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</span></a> <a href="https://mathstodon.xyz/tags/Teaching" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Teaching</span></a></p>
José A. Alonso<p>LeanTutor: A formally-verified AI tutor for mathematical proofs. ~ Manooshree Patel et als. <a href="https://arxiv.org/abs/2506.08321" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2506.08321</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> <a href="https://mathstodon.xyz/tags/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</span></a> <a href="https://mathstodon.xyz/tags/Teaching" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Teaching</span></a></p>
José A. Alonso<p>LeanTutor: A formally-verified AI tutor for mathematical proofs. ~ Manooshree Patel et als. <a href="https://arxiv.org/abs/2506.08321" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2506.08321</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/Teaching" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Teaching</span></a></p>
José A. Alonso<p>Rewriting SymCrypt in Rust to modernize Microsoft’s cryptographic library. ~ Brenda Potts. <a href="https://www.microsoft.com/en-us/research/blog/rewriting-symcrypt-in-rust-to-modernize-microsofts-cryptographic-library/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">microsoft.com/en-us/research/b</span><span class="invisible">log/rewriting-symcrypt-in-rust-to-modernize-microsofts-cryptographic-library/</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/RustLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>RustLang</span></a></p>
José A. Alonso<p>El futuro del razonamiento matemático: Integrando IA y Lean. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/11-el-futuro-del-razonamiento-matematico-integrando-ia-y-lean/" 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/11-el-futuro-del-razonamiento-matematico-integrando-ia-y-lean/</span></a> <a href="https://mathstodon.xyz/tags/IA" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IA</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> <a href="https://mathstodon.xyz/tags/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</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>Readings shared June 10, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/11-readings_shared_06-10-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/11-readings_shared_06-10-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/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</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/AlphaProof" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AlphaProof</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/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/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Prover9" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Prover9</span></a></p>
José A. Alonso<p>El proyecto ETP (Un caso de estudio en investigación matemática colaborativa y formalizada). <a href="https://jaalonso.github.io/vestigium/posts/2025/06/10-el-proyecto-etp-un-caso-de-estudio-en-investigacion-matematica-colaborativa-y-formalizada/" 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/10-el-proyecto-etp-un-caso-de-estudio-en-investigacion-matematica-colaborativa-y-formalizada/</span></a> <a href="https://mathstodon.xyz/tags/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</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>The equational theories project: advancing collaborative mathematical research at scale. ~ Terence Tao et als. <a href="https://terrytao.wordpress.com/wp-content/uploads/2025/06/math-experiments.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">terrytao.wordpress.com/wp-cont</span><span class="invisible">ent/uploads/2025/06/math-experiments.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> <a href="https://mathstodon.xyz/tags/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</span></a></p>
ExploreLive 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