Stars
A project to digitalise results from physics into Lean.
if your name is not Geoffrey Huntley then do not use loom
Fix three positive integers n, k, m Prove that a group subgroup H of S_{6+(n+k+m)} generated by g1:=G!(1,6,4,3,a_1,...a_n); g2:=G!(1,2,4,5,b_1,...,b_k); g3:=G!(5,6,2,3,c_1,...,c_m); H:=sub<G|[g1,g2…
A curated catalogue of awesome agentic AI patterns
A native elisp coding agent running in Emacs
Beads - A memory upgrade for your coding agent
Agentic AI Infrastructure for magnifying HUMAN capabilities.
💫 Toolkit to help you get started with Spec-Driven Development
From Zero to QED: An informal introduction to formality with Lean 4
Explicit solutions for the F- and R-symbols for the Drinfeld double of the Haagerup fusion category. Computed with the Julia package TensorCategories.jl
An implementation of the time dependent variational principle for matrix product states