Login

Recent searches

No recent searches

Search options

Only available when logged in.
fosstodon.org is one of the many independent Mastodon servers you can use to participate in the fediverse.
Fosstodon is an invite only Mastodon instance that is open to those who are interested in technology; particularly free & open source software. If you wish to join, contact us for an invite.

Administered by:

Server stats:

9.9K
active users

fosstodon.org: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#mathlib

0 posts0 participants0 posts today
Public
José A. Alonso

A semantic search engine for Mathlib4. ~ Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, Bin Dong. 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.
Public
Paul Schwahn

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 .

Public
José A. Alonso

A semantic search engine for Mathlib4. ~ Guoxiong Gao et als. 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.
ExploreLive feeds
About