Lists (1)
Stars
A Lean4 script for robustly verifying submitted proofs of theorems and implementations of functions
Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4
Tool to generate markdown files from lean files. This is heavily inspired by lean2md.
Interactive React-powered charting library for Lean 4 in VS Code's infoview
Levi-Civita field implementation in Lean 4 for computing with infinities and infinitesimals.
Terminal-based data visualization library for Lean 4. Port of Granite (Haskell) with type-safe guarantees. Create beautiful charts using Unicode braille characters.
This script can check and auto-generate `import` statements in a lean4 repository.
ASCII/Unicode plotting library for Lean 4 with legends and braille rendering
Absurdly sophisticated proofs of simple mathematical facts in Lean 4
Lean 4 port of the Golitex typesetting system for LaTeX-like document processing
Automatic differentiation in Lean following JAX's autodidax tutorial
General-relativistic raytracer in Lean 4 with geometric algebra for black hole visualization
Lean 4 port of Kôika: rule-based hardware description language with Verilog backend
Levi-Civita numbers for Lean 4 - infinitesimals and automatic differentiation
Type-safe property-based testing for Lean 4 powered by Python's Hypothesis framework
Lean 4 port of 'Coq: The World's Best Macro Assembler' - a verified x86 assembler
Verso documentation roles for Coq/Flocq references in literate Lean 4
Functional Programming in Lean book exercises with monad transformers
Functional assembly language written in Lean 4 with strong typing
PPM (Portable Pixmap) DSL for Lean 4 with custom syntax and ProofWidgets integration
A Lean 4 linter that detects unnecessary partial keywords in definitions
Git-backed issue tracker in Lean 4 - agent-friendly CLI with JSON output
SciLean extensions: Egyptian fractions, Lisp compiler, units of measurement
SIMD-accelerated string operations for Lean 4 via FFI to StringZilla