Software

murmel GitHub | Hugging Face

murmel is a search tool for Lean’s mathlib. It combines lightweight lexical search over declaration names, modules, and source snippets with semantic search based on a trained retriever. It also supports natural-language descriptions of declarations and keeps all artifacts keyed to the underlying mathlib commit, so queries stay tied to a precise revision of the library.

formurmel GitHub

formurmel is a Lean 4 formalization agent runtime. It runs tool-using LLMs against mathlib, using murmel for mathlib search and inspection, Lean for checking candidate snippets, and a mutable knowledge base for problem state.

riemaNN GitHub

riemaNN is research software for finding Einstein metrics with neural networks. It represents Riemannian metrics chartwise on finite atlases, glues local models across overlaps, and optimizes curvature-based objectives such as the traceless-Ricci L2 energy on spheres, sphere products, complex projective spaces, and connected sums.