José A. Alonso<p>Readings shared July 19, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/20-readings_shared_07-19-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/07/20-readings_shared_07-19-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/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/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/Mathlib" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Mathlib</span></a> <a href="https://mathstodon.xyz/tags/Reasoning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Reasoning</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a></p>
#mathlib
0 posts0 participants0 posts today
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
All tactics in mathlib4. ~ Haruhisa Enomoto. https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md #ITP #LeanProver #Mathlib
GitHubmathlib4-all-tactics/all-tactics.md at main · haruhisa-enomoto/mathlib4-all-tacticsMarkdown file of the list and explanations of all mathlib4 tactics - haruhisa-enomoto/mathlib4-all-tactics