Lists (1)
Starred repositories
The official GitHub page for the survey paper "A Survey on LLM Symbolic Reasoning". And this paper is under review.
A minimal language for Isabelle/HOL, designed for easing machine learning.
Lean 4 theorem proving skill and workflow pack for AI coding agents
[ICLR 2026] Lean Finder: Semantic Search For Mathlib That Understands User Intents
Development monorepo for Hex: verified computational algebra in Lean 4 (polynomial factoring, LLL, and friends). Released aggregate: https://github.com/leanprover/hex
Verified computational algebra in Lean 4: aggregator for the released hex libraries
First order model theory inside a topos in Lean
Information theory and hypothesis testing, in Lean
Some theorems presented to first and second year mathematics undergraduates, First and second year undergraduate level mathematics
Files associated with the course Interactive Theorem Proving at LMU SoSe 2025
Lean 4 formalization of Knuth's 'Claude's Cycles' paper
A repo to document candidate solutions for Erdős problems produced via LLM-driven proof search
Aristotle AI plugin for Claude Code - theorem proving and code verification with Lean 4
Setup for autograding of Lean homework using GitHub Classroom
Basic discrete probability and information theory in Lean
Lean 4 tactic library for closing proofs across applied mathematics. Probability, statistics, biology, chemistry, economics, engineering, mechanics, control, queueing, info theory. Axiom-clean agai…
MA4N1 Theorem Proving with Lean
A formal proof of an exponentially better upper bound on Ramsey numbers
Suggested conventions and examples for Lean formalization of IMO problem statements
Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)