Formally verified physics and mathematics in Lean 4 — from quantum mechanics to rotating black holes to rough path theory, built on Mathlib.
Logos libraries function is changing and is currently under construction. The QM machinery has moved and is available here.