José A. Alonso<p>Making concurrent hardware verification sequential. ~ Thomas Bourgeat, Jiazheng Liu, Adam Chlipala, Arvind. <a href="https://dl.acm.org/doi/pdf/10.1145/3729331" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">dl.acm.org/doi/pdf/10.1145/372</span><span class="invisible">9331</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/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CoqProver</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</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:
508active users
101010.pl: About · Status · Profiles directory · Privacy policy
Mastodon: About · Get the app · Keyboard shortcuts · View source code · v4.4.0-beta.2
#itp
32 posts · 7 participants · 5 posts today
José A. Alonso<p>Reviving DSP for advanced theorem proving in the era of reasoning models. ~ Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, Fan Yang. <a href="https://arxiv.org/abs/2506.11487v1" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2506.11487v1</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/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/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></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>Chomsky-Schützenberger representation theorem (in Isabelle/HOL). ~ Moritz Roos. <a href="https://www.isa-afp.org/entries/Chomsky_Schuetzenberger.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">isa-afp.org/entries/Chomsky_Sc</span><span class="invisible">huetzenberger.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>Reseña de «Can A.I. quicken the pace of math discovery?». <a href="https://jaalonso.github.io/vestigium/posts/2025/06/19-can-ai-quicken-the-pace-of-math-discovery/" 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/19-can-ai-quicken-the-pace-of-math-discovery/</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/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/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>Galois energy games (in Isabelle/HOL). ~ Caroline Lemke. <a href="https://www.isa-afp.org/entries/Galois_Energy_Games.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">isa-afp.org/entries/Galois_Ene</span><span class="invisible">rgy_Games.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 17, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/18-readings_shared_06-17-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/18-readings_shared_06-17-25</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/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>LeanHammer: an automated reasoning tool for Lean which combines multiple techniques for proof search and formal reconstruction. ~ Joshua Clune et als. <a href="https://github.com/JOSHCLUNE/LeanHammer" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">github.com/JOSHCLUNE/LeanHamme</span><span class="invisible">r</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 16, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/17-readings_shared_06-16-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/17-readings_shared_06-16-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/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/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a></p>
José A. Alonso<p>Toward a formalization of secure multiparty computation stack. ~ Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikaaw. <a href="https://www.math.nagoya-u.ac.jp/~garrigue/papers/weng-ppl2025.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">math.nagoya-u.ac.jp/~garrigue/</span><span class="invisible">papers/weng-ppl2025.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/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CoqProver</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>An approach to formalize information-theoretic security of multiparty computation protocols. ~ Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. <a href="https://www.math.nagoya-u.ac.jp/~garrigue/papers/weng-forte2025.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">math.nagoya-u.ac.jp/~garrigue/</span><span class="invisible">papers/weng-forte2025.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/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</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>LeanExplore: A search engine for Lean 4 declarations. ~ Justin Asher. <a href="https://arxiv.org/abs/2506.11085" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2506.11085</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>Readings shared June 15, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/16-readings_shared_06-15-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/16-readings_shared_06-15-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/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/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Lisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lisp</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/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a></p>
José A. Alonso<p>Reseña de «Hardest problems in mathematics, physics & the future of AI». <a href="https://jaalonso.github.io/vestigium/posts/2025/06/15-hardest-problems-in-mathematics-physics-the-future-of-ai/" 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-hardest-problems-in-mathematics-physics-the-future-of-ai/</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/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AI</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>BiCoq: Bigraphs formalisation with Coq. ~ Cécile Marcon et als. <a href="https://www.dcs.gla.ac.uk/~michele/papers/SAC2025.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">dcs.gla.ac.uk/~michele/papers/</span><span class="invisible">SAC2025.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/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CoqProver</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/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>Collaboration and innovation in the Equational Theories Project: Formalizing mathematics with Lean 4. ~ Marco Petracci. <a href="https://amslaurea.unibo.it/id/eprint/35220/1/TESI_MAGISTRALE_MARCO_PETRACCI-finale.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">amslaurea.unibo.it/id/eprint/3</span><span class="invisible">5220/1/TESI_MAGISTRALE_MARCO_PETRACCI-finale.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 information theory in Lean 4: divergences, hypothesis testing and the data processing inequality. ~ Lorenzo Luccioli. <a href="https://amslaurea.unibo.it/id/eprint/32676/1/MasterThesis.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">amslaurea.unibo.it/id/eprint/3</span><span class="invisible">2676/1/MasterThesis.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>Readings shared June 13, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/14-readings_shared_06-13-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/14-readings_shared_06-13-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/Autoformalization" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Autoformalization</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/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>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/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/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/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</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