Proof Atlas
A geometric language for Lean proofs. Inspect expression structure, binding and recorded typing rules, with exact links to compiled terms.
Projects
Interactive scientific tools and numerical libraries. Methods and research findings are collected in the Lab.
Interactive tools
The geometry of shortest paths
Motion, the pendulum reduction, cut time and the classical SE(2) optimal synthesis, explained through interactive figures. Numerical illustrations retain their stated scope.
Stages of star formation
Collapse and embedded stellar formation, illustrated from published physics. The survey research has established no stellar-birth detector.
Software
Elliptic functions
Matlab and Octave implementations of elliptic integrals, Jacobi elliptic functions and theta functions. Native scripts support tensor arguments and complex variants without external symbolic libraries.
The same functions — \(K(k)\), \(\operatorname{sn}\), \(\operatorname{cn}\), \(\operatorname{dn}\) — appear in the site's work on elastica and elliptic geometry.