Stars
Natural language tactics to teach mathematics using Lean 4
The simplest, fastest repository for training/finetuning medium-sized GPTs.
DSPy: The framework for programming—not prompting—language models
An Open Source implementation of Notebook LM with more flexibility and features
Markdown file of the list and explanations of all mathlib4 tactics
Lets make video diffusion practical!
Lean formalization of the Kolmogorov extension theorem
Construction of a Brownian Motion in Lean
Do you worry that you'll get to the end of a good list and have nothing more, leaving you sad and starved of data? Worry no more!
The Classiq Library is the largest collection of quantum algorithms and applications. It is the best way to explore quantum computing software. We welcome community contributions to our Library 🙌
An unsupervised model merging algorithm for Transformers-based language models.
Mathport is a tool for porting Lean3 projects to Lean4
A library of results from Social Choice Theory, formalized in the Lean Theorem Prover.
LLMs as Copilots for Theorem Proving in Lean
blueprint for prime number theorem and more
A Lean 4 representation of the Rubik's Cube, some proofs about the representation, and a simple solution algorithm.
plasTeX plugin to build formalization blueprints.
Definitional implementation of Cedar language and utilities for DRT
Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)
Ongoing Lean formalisation of the proof of Fermat's Last Theorem