jsmorph

GPT 5.4 compiled these instructions from this blog post by Scott Armstrong about his and Julia Kempe's Lean 4 formalization of De Giorgi–Nash–Moser theory.

Armstrong's recent math formalization notes (as interpreted)

This skill is for formalization projects in mature parts of

jsmorph

import Project.Gcd.Program
import Interpreter.Wasm.Wp.Tactic
import Interpreter.Wasm.Wp.Block
import Interpreter.Wasm.Wp.Loop

/-!
# Specification for `gcd`
-/

namespace Project.Gcd.Spec

jsmorph

import Project.AssocList.Program
import Interpreter.Wasm.Wp.Tactic
import Interpreter.Wasm.Wp.Call

/-!
# Specification for `lookupDemo`
-/

namespace Project.AssocList.Spec

jsmorph

I want you to implement design.md. It should be utterly perfect, visually beautiful, with every single thing done at high quality.

Fan out sub-agents and have sub-agents tackle each one individually so that the app is utterly perfect. You should /loop on each item and have a separate sub-agent check it visually to ensure it looks triple A. That separate sub-agent should be a really harsh critic, and if it doesn't work very well, it should keep going.

Don't stop until each sub-agent is utterly wowed with the quality. It should literally compare them side by side blind and say which one looks better. /loop until it's utterly perfect. Fan out sub-agents and ultracode.

Keep me updated as you make progress but do not stop.

jsmorph

Notes

I'm speculating about a style of math research that might be satisfying and productive over the next few years (but not beyond that). If on target, then likely obvious.

Some caveats: I'm not a research mathematician, and I have had almost no training along those lines. My recent experience is with software with AI on all levels, but I'm skeptical of possible parallels.

jsmorph

/-
The baseline point-addition circuit followed by the verified transposition
implements addition in the full secp256k1 point group.
-/
import Tests.GroupTotalPointAddition.Transpose
import VQMathlib.Curve.GroupTotal

namespace VQ.Tests.GroupTotalPointAddition

open VQ VQ.Reversible