Tools based on AI for helping with Lean 4

A (WIP) equality saturation tactic for Lean based on egg.

aider is AI pair programming in your terminal

The SQL IDE for Your Terminal.

mngr – terminal-based database manager (TUI) for PostgreSQL, MariaDB/MySQL, MongoDB, SQLite, and JSON with vim-like keybindings

Fastest terminal UI for react (TUI, CLI, curses-like)

A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi,@lweqx]

A control flow graph library for Lean

Formalization of Arithmetization of Mathematics/Metamathematics

Formalizing results about the Mandelbrot set in Lean

Leaff is a diff tool for Lean environments

Siksek's chabnf code, souped up

Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Combinatorics in Lean

Work coming out of Dagstuhl seminar 23401

Linter component for Isabelle.

Python talking to the Lean theorem prover

Lindemann–Weierstrass Theorem

Functional Programming in Lean

Helper toolkit for creating your own Lean 4 UserWidgets

A guidance language for controlling large language models.

Server to host lean games.

vanity hex prefixes for your commit SHAs

Interfacing with Large Language Models (remote and local) from Lean.