Mathstodon

1 post1 participant0 posts today

LeanThe Lean FRO team met synchronously in Amsterdam last week for our annual team retreat, and to discuss upcoming work and our Year 3 roadmap! 🇳🇱✨We had very productive discussions around Lean's future in mathematics, software and hardware verification, and AI for math. It was energizing to see our team's commitment to Lean's continued growth in each of these domains.We're cooking up many exciting developments that will support both our mathematical community and our growing base of software verification users. Stay tuned for our full Y3 roadmap publication at the end of July!<a href="https://functional.cafe/tags/LeanLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanLang</a> <a href="https://functional.cafe/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://functional.cafe/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Lean4</a> <a href="https://functional.cafe/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a> <a href="https://functional.cafe/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Programming</a> <a href="https://functional.cafe/tags/Mathematics" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Mathematics</a> <a href="https://functional.cafe/tags/TheoremProving" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#TheoremProving</a>

Andreas Grois<a href="https://mastodon.gamedev.place/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Lean4</a> 4.19 has added mimalloc as an optional dependency. I am totally fine with this.However, I don't like that it just tries to download it during the build process, instead of looking for a system-installed version first.This means, my current Lean4 <a href="https://mastodon.gamedev.place/tags/Gentoo" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Gentoo</a> ebuild does not work with 4.19 any more...I will have to write a patch for Lean at some point, to allow using a locally installed mimalloc.

WinbuzzerDeepSeek Releases Massive 671B Prover V2 Model For Mathematical Theorem Proving Ahead of R2 Release<a href="https://mastodon.social/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AI</a> <a href="https://mastodon.social/tags/ChinaAI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ChinaAI</a> <a href="https://mastodon.social/tags/DeepSeek" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#DeepSeek</a> <a href="https://mastodon.social/tags/OpenSourceAI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#OpenSourceAI</a> <a href="https://mastodon.social/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a> <a href="https://mastodon.social/tags/TheoremProving" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#TheoremProving</a> <a href="https://mastodon.social/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Lean4</a> <a href="https://mastodon.social/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#MachineLearning</a> <a href="https://mastodon.social/tags/DeepLearning" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#DeepLearning</a> <a href="https://mastodon.social/tags/MathAI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#MathAI</a><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 noreferrer" translate="no" target="_blank">https://winbuzzer.com/2025/04/30/deepseek-releases-massive-671b-prover-v2-model-for-mathematical-theorem-proving-ahead-of-r2-release-xcxwbn/</a>

sheerluckuse <a href="https://misskey.io/tags/Lean4" rel="nofollow noopener noreferrer" target="_blank">#Lean4</a> for proofs please RE: <a href="https://mitra.do.rayslava.com/objects/01963ed0-f2ed-adbc-9c35-4f99b4bb4030" rel="nofollow noopener noreferrer" target="_blank">https://mitra.do.rayslava.com/objects/01963ed0-f2ed-adbc-9c35-4f99b4bb4030</a>

mehbark<a href="https://critter.cafe/tags/mathlib" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#mathlib</a> has a fascinating set of counterexamples, which includes, for example, a disproof of the Aharoni–Korman conjecture: <a href="https://leanprover-community.github.io/mathlib4_docs/Counterexamples/AharoniKorman.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://leanprover-community.github.io/mathlib4_docs/Counterexamples/AharoniKorman.html</a>when i'm in a <a href="https://critter.cafe/tags/lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#lean4</a> phase, i often think of (much, much more trivial) false statements, so i decided to just start proving that they were indeed false: <a href="https://g.pyrope.net/simple-counterexamples" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://g.pyrope.net/simple-counterexamples</a>the pace of additions will be somewhat rapid because the proofs are only a couple of lines at most. they're fun to think about, though—how would you prove that (haskell syntax) <code>Monad m => m a -> a</code> is inconsistent?

Mark Andrew Gerads<a href="https://www.youtube.com/watch?v=TFBzP78Jp6A" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://www.youtube.com/watch?v=TFBzP78Jp6A</a><a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="tag">#Lean4</a> <a href="https://mathstodon.xyz/tags/LeanLang" class="mention hashtag" rel="tag">#LeanLang</a> <a href="https://mathstodon.xyz/tags/Lean" class="mention hashtag" rel="tag">#Lean</a>

Andreas GroisTIL: <a href="https://mastodon.gamedev.place/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Lean4</a> Substring.isEmpty == false does not imply Substring.toString.isEmpty == false.The problem arises because Substring.isEmpty only looks if the difference between start/stop position is zero. It does not check, if those positions are inside the underlying string.It is therefore easy to produce a Substring that has Substring.isEmpty == false, but Substring.toString.isEmpty == true.<a href="https://live.lean-lang.org/#codez=CYUwZgBCEFwLwQBQGUCuAjAzgFwE4EsA7AcwDoBbAawgCIBDTYMGpZPIsgBQHtMLqArAEpW7EqR58qEAGxChAKAUBaZRDB0ANphAKAxCABuWqKXyYAouQAO2AJ5LVEPKl0Hjm09m5sC481a2dkA" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://live.lean-lang.org/#codez=CYUwZgBCEFwLwQBQGUCuAjAzgFwE4EsA7AcwDoBbAawgCIBDTYMGpZPIsgBQHtMLqArAEpW7EqR58qEAGxChAKAUBaZRDB0ANphAKAxCABuWqKXyYAouQAO2AJ5LVEPKl0Hjm09m5sC481a2dkA</a>

Adolfo NetoWill you be in Oxford on May 6? You can attend Leonardo de Moura's lecture on Lean! <a href="https://bertha.social/tags/LeanLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanLang</a> <a href="https://bertha.social/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://bertha.social/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Lean4</a>

Hacker NewsClean, a formal verification DSL for ZK circuits in Lean4<a href="https://blog.zksecurity.xyz/posts/clean/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://blog.zksecurity.xyz/posts/clean/</a><a href="https://mastodon.social/tags/HackerNews" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#HackerNews</a> <a href="https://mastodon.social/tags/Clean" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Clean</a> <a href="https://mastodon.social/tags/ZK" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ZK</a> <a href="https://mastodon.social/tags/circuits" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#circuits</a> <a href="https://mastodon.social/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Lean4</a> <a href="https://mastodon.social/tags/formal" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formal</a> <a href="https://mastodon.social/tags/verification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#verification</a> <a href="https://mastodon.social/tags/DSL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#DSL</a>

sheerluck<a href="https://misskey.io/tags/Lean4" rel="nofollow noopener noreferrer" target="_blank">#Lean4</a> or <a href="https://misskey.io/tags/Idris2" rel="nofollow noopener noreferrer" target="_blank">#Idris2</a> RE: <a href="https://msk.seppuku.club/notes/a5s7w4w8gz" rel="nofollow noopener noreferrer" target="_blank">https://msk.seppuku.club/notes/a5s7w4w8gz</a>

Hacker NewsFormal Verification for Machine Learning Models Using Lean 4<a href="https://github.com/fraware/leanverifier" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/fraware/leanverifier</a><a href="https://mastodon.social/tags/HackerNews" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#HackerNews</a> <a href="https://mastodon.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a> <a href="https://mastodon.social/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#MachineLearning</a> <a href="https://mastodon.social/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Lean4</a> <a href="https://mastodon.social/tags/AIResearch" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AIResearch</a> <a href="https://mastodon.social/tags/TechInnovation" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#TechInnovation</a>

TariqI'll be doing a short beginner-friendly intro and live-demo of the Lean + Mathlib maths proof system at the next <a href="https://mastodon.social/tags/pydata" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#pydata</a> <a href="https://mastodon.social/tags/exeter" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#exeter</a> meetup in early April <a href="https://www.meetup.com/pydata-exeter/events/306511193/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.meetup.com/pydata-exeter/events/306511193/</a><a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/lean" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#lean</a> <a href="https://mastodon.social/tags/lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#lean4</a>

TariqAfter months of working daily, today at 5.02pm approx I completed the course" Mechanics of Proof "That's means I completed every exercise - (except 3)When I started I wanted to learn cover the basis of not just algebra, but also sets and functions - and the course does that. The only area it doesn't cover that I wanted was real analysis - eg convergence of sequences etcphew !<a href="https://hrmacbeth.github.io/math2001/index.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://hrmacbeth.github.io/math2001/index.html</a><a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/lean" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#lean</a> <a href="https://mastodon.social/tags/lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#lean4</a>

TariqIf you think writing maths proofs in code is only for PhDs...... this course was created for you!* small bite-size examples * concepts first, code second * minimal jargon * one simple exercise per chapter - designed to build confidence - not destroy it !<a href="https://www.amazon.com/dp/B0DWHS1RDJ" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.amazon.com/dp/B0DWHS1RDJ</a><a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/lean" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#lean</a> <a href="https://mastodon.social/tags/lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#lean4</a>

Lukas GerlachMy Existential Rule <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="tag">#Lean4</a> library [1] is taking shape more and more. I've recently finished a correctness proof for a sufficient condition for chase termination, called MFA. I'm hopeful that extensions of this notion (DMFA and RMFA) are not too hard to formalize now once a few ugly technicalities are sorted out :)[1] <a href="https://github.com/monsterkrampe/Existential-Rules-in-Lean" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://github.com/monsterkrampe/Existential-Rules-in-Lean</a>

jnkrtechI'm still fumbling about in the dark with Lean, but my goal for my first big project is to implement system F sub omega and prove its type safety. I'm going to try some simpler lambda calculi first, probably, because I fear that which I do not understand.Question: Does anyone have tips/examples/guides as to how to start to practically describe a type theory? I started out trying to define evaluation and de Bruijn indices etc and got lost in the weeds. Is there a way to operate fully at a higher level, and only really talk about the types? And if I'm only interested in proving the theory, and not with efficient execution, is there a better way for me to represent scopes/contexts?<a href="https://social.treehouse.systems/tags/lean" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#lean</a> <a href="https://social.treehouse.systems/tags/programminglanguagetheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#programminglanguagetheory</a> <a href="https://social.treehouse.systems/tags/PLT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#PLT</a> <a href="https://social.treehouse.systems/tags/proofs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#proofs</a> <a href="https://social.treehouse.systems/tags/TAPL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#TAPL</a> <a href="https://social.treehouse.systems/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Lean4</a>

sheerluck<a href="https://misskey.io/tags/Lean4" rel="nofollow noopener noreferrer" target="_blank">#Lean4</a> Feature Request: rofl as alias to rfl

sheerluck<a href="https://misskey.io/tags/Stockfish" rel="nofollow noopener noreferrer" target="_blank">#Stockfish</a> <a href="https://misskey.io/tags/HaChu" rel="nofollow noopener noreferrer" target="_blank">#HaChu</a> <a href="https://misskey.io/tags/Lean4" rel="nofollow noopener noreferrer" target="_blank">#Lean4</a> <a href="https://misskey.io/tags/exact" rel="nofollow noopener noreferrer" target="_blank">#exact</a> <a href="https://misskey.io/tags/exactly" rel="nofollow noopener noreferrer" target="_blank">#exactly</a> <a href="https://misskey.io/tags/gptf" rel="nofollow noopener noreferrer" target="_blank">#gptf</a> <a href="https://misskey.io/tags/Loogle" rel="nofollow noopener noreferrer" target="_blank">#Loogle</a>

Jon SterlingSome strange behaviour with Lean's evaluation of thunks. I wonder if is intentional that this result in [[forcing]] being printed twice?Keep in mind that if I do a variation on this without using an inductive type constructor, [[forcing]] is printed only once.<a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="tag">#Lean4</a> <a href="https://mathstodon.xyz/tags/Lean" class="mention hashtag" rel="tag">#Lean</a>

Tariq"Constructing proofs is an art, checking them is a science."If you're new to writing proofs as code, check out my course designed to build confidence - not demolish it!<a href="https://www.amazon.com/dp/B0DWHS1RDJ" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.amazon.com/dp/B0DWHS1RDJ</a><a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/lean" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#lean</a> <a href="https://mastodon.social/tags/lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#lean4</a>

Recent searches

Search options

Administered by:

Server stats:

#Lean4