Lists (1)
Starred repositories
Turn your documents into a Markdown wiki you can read, that answers with citations. Works with any LLM provider, Ollama included. CROW: 99.5% right note read vs 79%, 1.6× faster ingest, 63% fewer L…
Jev-like family of decision models built on top of Qwen3.5/3.8 you can train and run on your own
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.
Formalized mathematics from textbooks and research papers in Lean 4.
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
LLM-driven proof search on Erdős problems (2 solutions accepted on erdosproblems.com)
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
4CB8
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