Tool for data extraction and interacting with Lean programmatically.

Visualizing the network of math theories.

Code for Parsel 🐍 - generate complex programs with language models

Retrieval-Augmented Theorem Provers for Lean

eGenix PyRun - Your friendly, lean, open source Python runtime

llmstep: [L]LM proofstep suggestions in Lean 4.

ChatGPT plugin for theorem proving in Lean

Tiny theorem prover with syntax like Lean 4 in <1K LOC

List of the output of #help command of mathlib4, including list of all tactics, commands...etc

Read README for more information.

System-wide Lean input method

A comprehensive collection of mathematical tools and utilities designed to support Lean Six Sigma practitioners in their process improvement journey

Autoformalization of coding problems, verified with test cases

A work-in-progress Lean 4 binding to GiNaC

a system for analyzing and repairing arguments

Measuring the growth of open source formal methods

Automatically updated API documentation for QuantConnect's Lean

DSPy + Lean (mock) iterative prover with hint clipping; sweeps on clipping vs KL, noise, sparsity; scalable dataset generator; curated training; frozen tools.

A set of Python scripts to extract and analyze lemmas, theorems, and definitions from LEAN 4 source files.

aol?