Recent searches

No recent searches

Search options

Only available when logged in.
med-mastodon.com is one of the many independent Mastodon servers you can use to participate in the fediverse.
Medical community on Mastodon

Administered by:

Server stats:

372
active users

med-mastodon.com: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.1

#lean4

0 posts0 participants0 posts today
José A. Alonso<p>Readings shared June 6, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/06-readings_shared_06-06-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/06-readings_shared_06-06-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/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</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>Libro "Matemáticas en Lean4" (versión del 6-junio-25). <a href="https://raw.githubusercontent.com/jaalonso/Matematicas_en_Lean4/main/Matematicas_en_Lean4.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">raw.githubusercontent.com/jaal</span><span class="invisible">onso/Matematicas_en_Lean4/main/Matematicas_en_Lean4.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/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
Terence Tao<p>A third video in my occasional series on <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> formalization workflows, this time focusing on how relying extensively on <a href="https://mathstodon.xyz/tags/GitHubCopilot" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>GitHubCopilot</span></a> fares against standard "epsilon delta" type problems in analysis. <a href="https://www.youtube.com/watch?v=c1ixXMtmfS8" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">youtube.com/watch?v=c1ixXMtmfS</span><span class="invisible">8</span></a></p>
Winbuzzer<p>DeepSeek Releases Massive 671B Prover V2 Model For Mathematical Theorem Proving Ahead of R2 Release</p><p><a href="https://mastodon.social/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AI</span></a> <a href="https://mastodon.social/tags/ChinaAI" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ChinaAI</span></a> <a href="https://mastodon.social/tags/DeepSeek" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>DeepSeek</span></a> <a href="https://mastodon.social/tags/OpenSourceAI" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>OpenSourceAI</span></a> <a href="https://mastodon.social/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mastodon.social/tags/TheoremProving" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TheoremProving</span></a> <a href="https://mastodon.social/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mastodon.social/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MachineLearning</span></a> <a href="https://mastodon.social/tags/DeepLearning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>DeepLearning</span></a> <a href="https://mastodon.social/tags/MathAI" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MathAI</span></a></p><p><a href="https://winbuzzer.com/2025/04/30/deepseek-releases-massive-671b-prover-v2-model-for-mathematical-theorem-proving-ahead-of-r2-release-xcxwbn/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">winbuzzer.com/2025/04/30/deeps</span><span class="invisible">eek-releases-massive-671b-prover-v2-model-for-mathematical-theorem-proving-ahead-of-r2-release-xcxwbn/</span></a></p>
Hacker News<p>Clean, a formal verification DSL for ZK circuits in Lean4</p><p><a href="https://blog.zksecurity.xyz/posts/clean/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">blog.zksecurity.xyz/posts/clea</span><span class="invisible">n/</span></a></p><p><a href="https://mastodon.social/tags/HackerNews" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HackerNews</span></a> <a href="https://mastodon.social/tags/Clean" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Clean</span></a> <a href="https://mastodon.social/tags/ZK" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ZK</span></a> <a href="https://mastodon.social/tags/circuits" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>circuits</span></a> <a href="https://mastodon.social/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mastodon.social/tags/formal" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>formal</span></a> <a href="https://mastodon.social/tags/verification" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>verification</span></a> <a href="https://mastodon.social/tags/DSL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>DSL</span></a></p>
Jon Sterling<p>Some strange behaviour with Lean's evaluation of thunks. I wonder if is intentional that this result in [[forcing]] being printed twice?</p><p>Keep in mind that if I do a variation on this without using an inductive type constructor, [[forcing]] is printed only once.</p><p><a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/Lean" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean</span></a></p>
José A. Alonso<p>Readings shared January 21, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/21-readings_shared_01-21-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/01/21-readings_shared_01-21-25</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/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</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/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Prolog</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LogicProgramming</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></p>
José A. Alonso<p>Proofs of the Praeclarum Theorema in Lean4 and Isabelle/HOL. <a href="https://jaalonso.github.io/calculemus/posts/2025/01/21-praeclarum_theorema/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2025/01/21-praeclarum_theorema/</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/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</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/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a></p>
José A. Alonso<p>Lean: First steps (22 - Recursion) [Video]. ~ Tariq Rashid. <a href="https://youtu.be/McHUB7pyj6I" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/McHUB7pyj6I</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/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</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: First steps (22 - Recursion). ~ Tariq Rashid. <a href="https://leanfirststeps.blogspot.com/2025/01/22-recursion.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">leanfirststeps.blogspot.com/20</span><span class="invisible">25/01/22-recursion.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/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</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 January 6, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/06-readings_shared_01-06-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/01/06-readings_shared_01-06-25</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/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</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/HoTT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HoTT</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/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></p>
José A. Alonso<p>Lean: First steps (21 - Simple induction). ~ Tariq Rashid (<span class="h-card" translate="no"><a href="https://mastodon.social/@rzeta0" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>rzeta0</span></a></span>). <a href="https://youtu.be/E55hdgQTcms" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/E55hdgQTcms</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/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</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 January 3, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/03-readings_shared_01-03-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/01/03-readings_shared_01-03-25</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/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</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/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</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> <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/OCaml" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>OCaml</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/Python" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Python</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/MachineLearning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MachineLearning</span></a></p>
José A. Alonso<p>Proofs of the Nicomachus’s theorem in Lean4 and Isabelle/HOL. <a href="https://jaalonso.github.io/calculemus/posts/2025/01/03-nicomachus_theorem/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2025/01/03-nicomachus_theorem/</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/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</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/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a></p>
José A. Alonso<p>Readings shared January 1, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/01-readings_shared_01-01-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/01/01-readings_shared_01-01-25</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/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Mizar</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/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/Python" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Python</span></a></p>
José A. Alonso<p>Lean: First steps (21 - Simple induction). ~ Tariq Rashid (<span class="h-card" translate="no"><a href="https://mastodon.social/@rzeta0" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>rzeta0</span></a></span>). <a href="https://leanfirststeps.blogspot.com/2024/12/21-induction.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">leanfirststeps.blogspot.com/20</span><span class="invisible">24/12/21-induction.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/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</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 December 25, 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/12/25-readings_shared_12-25-24" 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/2024/12/25-readings_shared_12-25-24</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/Python" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Python</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/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</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/Programming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Programming</span></a></p>
José A. Alonso<p>Lean: First steps (20 - Contradictory cases). ~ Tariq Rashid (<span class="h-card" translate="no"><a href="https://mastodon.social/@rzeta0" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>rzeta0</span></a></span>). <a href="https://leanfirststeps.blogspot.com/2024/12/20-contradictory-cases.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">leanfirststeps.blogspot.com/20</span><span class="invisible">24/12/20-contradictory-cases.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/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</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 December 16, 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/12/16-readings_shared_12-16-24" 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/2024/12/16-readings_shared_12-16-24</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/LeanLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanLang</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</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/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> # <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/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CommonLisp</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/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></p>
José A. Alonso<p>Lean: First steps (19 - Reductio ad absurdum). ~ Tariq Rashid (<span class="h-card" translate="no"><a href="https://mastodon.social/@rzeta0" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>rzeta0</span></a></span>). <a href="https://leanfirststeps.blogspot.com/2024/12/19-reductio-ad-absurdum.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">leanfirststeps.blogspot.com/20</span><span class="invisible">24/12/19-reductio-ad-absurdum.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/LeanLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanLang</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
TrendingLive feeds
About