#mathlib
0 posts0 participants0 posts today
Readings shared May 10, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/10-readings_shared_05-10-25 #ITP #LeanProver #Math #Mathlib #Python
Vestigium · Readings shared May 10, 2025The readings shared in Bluesky on 10 May 2025 are
A tool to verify estimates, II: a flexible proof assistant. ~Terence Tao. #ITP #Python #Math
How to (actually) prove it - New frontiers of mathematic
LeanExplore: a new Mathlib search engine that combines semantic search embeddings, AI-generated translations, and PageRank to give optimized search results. https://www.leanexplore.com/ #ITP #LeanProver #Mathlib
www.leanexplore.comLeanExplore
Basic probability in Mathlib. ~ Rémy Degenne. https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/ #ITP #LeanProver #Mathlib #Math
Lean community blog · Basic probability in MathlibHow do I define a probability space and two independent random variables in Lean? Should I use IsProbabilityMeasure or ProbabilityMeasure?
How do I condition on an event?
This post answers these and o
" 𝗠𝗮𝘁𝗵𝘀 𝗣𝗿𝗼𝗼𝗳𝘀 𝗶𝗻 𝗟𝗲𝗮𝗻 - 𝗙𝗶𝗿𝘀𝘁 𝗦𝘁𝗲𝗽𝘀 " 
Designed specifically for beginners struggling to get started with other courses and guides.
* Simple bite-sized examples.
* Focus on concepts, introduced gradually.
* One easy exercise per chapter.
.. all to build confidence, not demolish it !
... it's out !
" Maths Proofs in Lean - First Steps "
Designed specifically for newcomers and beginners struggling to get started with other courses and guides.
* Simple bite-sized examples explained.
* Concepts introduced gradually.
* One easy exercise per chapter.
.. all to build confidence, not demolish it !
Readings shared February 5, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/05-readings_shared_02-05-25 #ITP #IsabelleHOL #LeanProver #Mathlib #LLMs #Math
Vestigium · Readings shared February 5, 2025The readings shared in Bluesky on 5 February 2025 are
On the cofinality property in the context of the hierarchy of decreasing Church-Rosser abstract rewriting systems. ~ Ievgen Ivanov. #ITP #Isabell
A semantic search engine for Mathlib4. ~ Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, Bin Dong. https://arxiv.org/abs/2403.13310 #ITP #LeanProver #Mathlib
arXiv.orgA Semantic Search Engine for Mathlib4The interactive theorem prover Lean enables the verification of formal mathematical proofs and is backed by an expanding community. Central to this ecosystem is its mathematical library, mathlib4, which lays the groundwork for the formalization of an expanding range of mathematical theories. However, searching for theorems in mathlib4 can be challenging. To successfully search in mathlib4, users often need to be familiar with its naming conventions or documentation strings. Therefore, creating a semantic search engine that can be used easily by individuals with varying familiarity with mathlib4 is very important. In this paper, we present a semantic search engine (https://leansearch.net/) for mathlib4 that accepts informal queries and finds the relevant theorems. We also establish a benchmark for assessing the performance of various search engines for mathlib4.
As a step towards computer-formalizing the classification of low-dimensional Lie algebras, we finally formalized our first non-boring theorem in #Lean4 !
If L is a 3-dimensional Lie algebra (over any field) with a one-dimensional commutator subalgebra which is contained in the center of L, then L is isomorphic to the 3D Heisenberg algebra - that is, it has a basis (𝑒₀, 𝑒₁, 𝑒₂) such that the bracket is determined by
[𝑒₁,𝑒₂]=𝑒₀,
[𝑒₀,𝑒₁]=0,
[𝑒₀,𝑒₂]=0.
Now we're working on the analogous results for higher dimensional commutator subalgebras. These are going to be harder because
a) there's no one-size-fits-all classification statement for arbitrary fields, and
b) they rely on certain normal forms of matrices which aren't yet implemented in #mathlib .
The Matrix Cookbook, using Lean's mathlib. ~ Eric Wieser. https://github.com/eric-wieser/lean-matrix-cookbook #ITP #LeanProver #Lean4 #Mathlib #Math
GitHubGitHub - eric-wieser/lean-matrix-cookbook: The matrix cookbook, proved in the Lean theorem proverThe matrix cookbook, proved in the Lean theorem prover - eric-wieser/lean-matrix-cookbook
Readings shared September 21, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/21-readings_shared_09-21-24 #ITP #IsabelleHOL #LeanProver #Lean3 #Lean4 #Mathlib #Logic #Math #AI #LLMs #DeepLearning
Vestigium · Readings shared September 21, 2024The readings shared in Mastodon on September 21, 2024 are
Readings shared September 20, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #ATP #Prover9 #Mace4
Course: Theorem proving with Lean. ~ Dami
Finding lemmas in Mathlib. ~ Damiano Testa. https://github.com/adomani/MA4N1_Theorem_proving_with_Lean/blob/master/MA4N1_2023/L17_navigating_Mathlib.lean #ITP #LeanProver #Mathlib
GitHubMA4N1_Theorem_proving_with_Lean/MA4N1_2023/L17_navigating_Mathlib.lean at master · adomani/MA4N1_Theorem_proving_with_LeanMA4N1 Theorem Proving with Lean. Contribute to adomani/MA4N1_Theorem_proving_with_Lean development by creating an account on GitHub.
Lecturas compartidas el 1 de agosto de 2024. https://jaalonso.github.io/vestigium/posts/2024/08/02-lecturas_compartidas_el_01-ago-24 #ITP #Lean4 #Mathlib #Coq #Math #Haskell #FunctionalProgramming
Vestigium · Lecturas compartidas el 1 de agosto de 2024Las lecturas compartidas en Mastodon el 1 de agosto de 2024 son
Lecturas compartidas el 31 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #LLMs #ATP #Reasoning
Continuous functions — formali
Search Mathlib: A webpage that searches for Mathlib theorems. ~ Deming Xu. https://huggingface.co/spaces/dx2102/search-mathlib #ITP #Lean4 #Mathlib
huggingface.coSearch Mathlib - a Hugging Face Space by dx2102Discover amazing ML apps made by the community
LeanSearch: Find theorems in Mathlib4 using natural language query. https://leansearch.net #ITP #Lean4 #Mathlib
leansearch.netMathlib4 Search
This month in Mathlib (May 2024). https://leanprover-community.github.io/blog/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/ #ITP #Lean4 #Mathlib #Math
Lean community blog · This month in Mathlib (May 2024)The last Month in Mathlib posts date from before the port started, in November 2022. We apologise for the momentary disappearance. We aim to keep it a monthly occurrence from now on.
There were 667 PR