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

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

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

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

/-!
# Specification for `lookupDemo`
-/

namespace Project.AssocList.Spec

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

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

namespace EthereumVm

inductive OpCode where
  | STOP
  | ADD
  | MUL
  | PUSH1 (value : UInt8)
  | MLOAD
  | MSTORE
  | MSTORE8

jsmorph

jsmorph

y@dev20210711:~/src/quamina$ quaminagen -h
Usage of quaminagen:
  -core
    	use CoreMatcher instead of Pruner
  -matching-events int
    	number of matching events (default 1000)
  -matching-patterns int
    	number of Matching patterns (default 1000)
  -num-pattern-ids int
    	number of pattern ids (default 400)

jsmorph

package quamina

import (
	"fmt"
	"log"
	"math/rand"
	"sync"
	"testing"
)