LeanArchitect extracts a blueprint directly from Lean source.

The Noperthedron does not have Rupert Property: a proof in Lean4

Advanced data visualization with Typst.

Lean-Yjs: Formal Verification of Yjs Integration Algorithm

Type theories as quotient inductive-inductive-recursive types

A formalized proof of a version of the initiality conjecture

Manage your macOS using Nix

Generate Talmudic page layouts.

Binary Decision Diagrams in Lean 4

Mechanization of Synthetic Tait Computability in Istari

An experimental mutual induction tactic for Lean 4.

Formalization of the Rupert Problem for convex polyhedra.

Exceptions to the ABC conjecture in Lean

Logical Relation for MLTT in Coq

Automata for decision procedures in Lean

An extension of the NbE algorithm to produce computational traces

Ground Zero: Lean 4 HoTT Library

An evaluation benchmark for undergraduate competition math in Lean4, Isabelle, Coq, and natural language.

A translation framework for eliminating definitional equalities in Lean

First order model theory inside a topos in Lean

Formalizing Fibered Categories and Stacks in Lean

better braids

Lean 4 kernel / 'external checker' written in Lean 4

==> ARDUTOUCH KITS ARE AVAILABLE at CornfieldElectronics.com <== ArduTouch is an Arduino-compatible music synthesizer kit with a built-in touch keyboard, and with built-in speaker/amplifier. Build …