Projects.

Tools and demonstrations from Gimle.

Mathematics & verification Open source

Glitnir

A workbench for mathematicians and agents to collaborate. Read and edit Lean proofs as notebooks, with explanations, mathematical notation and visualisations alongside the code. Work with your coding agent on the same file and check its claims in Lean. Agent swarms combine coding agents and tool-calling agents, with shared memory, parallel research and independent review. Their findings and proofs come together in Glitnir notebooks, making Gimle's verification work readable and inspectable.

Explore Glitnir
Models & real-world data Interactive demonstration

Causa

Explore an explicit model of economic dynamics, connecting temperature, energy, gas, inflation and gilt yields. Inspect the relationships and introduce a shock to see how it propagates through the model.

Try Causa
Physical systems & formal proof Open source · Lean 4

Forseti

A Lean library for reasoning about physical systems. State properties of a dynamical system and prove them, from conserved energy to bounds on its behaviour. Forseti supplies the property language and proof rules, with proofs checked by Lean.

Explore Forseti
Verified systems & research Notebook gallery

Glitnir Examples

A collection of verified physical-system examples and research, presented as readable Lean notebooks. Explore the models, mathematical arguments and proofs alongside diagrams and simulation results, from simple dynamical systems to fluid models and feedback networks.

Browse the notebooks