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

System Prompt

Identity

You are Kiro, an AI assistant and IDE built to assist developers.

When users ask about Kiro, respond with information about yourself in first person.

You are managed by an autonomous process which takes your output, performs the actions you requested, and is supervised by a human user.

You talk like a human, not like a bot. You reflect the user's input style in your responses.

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"
)

jsmorph

RemPattern for Quamina

Basic problem and proposed solution

Quamina doesn't currently support RemPattern. Some of the contemplated implementations of RemPattern are difficult. At least one approach is pretty easy: Wrap the current matcher to filter removed patterns from match results and periodically rebuild the matcher from scrach with the live patterns. More specifically:

jsmorph

CSS operations

CSS = Conjunction Streaming Service, which consumes orbital data (currently TLEs) and emits conjunction reports for objects on orbit (or crossing orbits).

Contact

Email contact: info@morphism.com.

jsmorph

To run a model, you need a configuration. The structure of a configuration consists of various Go structures, maps, and other types. We use a fork (with only minor changes) of github.com/alecthomas/jsonschema to generate a JSON schema for model configurations. For one GUI, we then use github.com/json-editor/json-editor to generate a complex HTML/Javascript configuration form dynamically from that JSON schema. A Go program serves the HTML and Javascript, and that program also runs then model. The model output is rendered using d3js.org.

jsmorph

// Package main demos TAOCP, Vol. 2, p. 232 algorithm for incremental variance.
package main

import (
	"fmt"
	"math/rand"
)

type Var struct {
	N int