Lucas Rose-Winters
I'm an independent researcher working on formal verification, operating systems, programming languages, algebra and AI. My background is in application security and critical infrastructure.
Results
Read the results →27% less memory · July 20261.79×GPU prefill speed versus llama.cpp CUDAApeiron · Qwen2.5-0.5B Q4_K_M
512-token prompt · RTX 50801.11×GPU decode speed versus llama.cpp CUDAApeiron · Qwen2.5-0.5B Q4_K_M
128 generated tokens · RTX 5080
Work
All work →-
Research · active
Apeiron
Rust algebra primitives with Lean proofs, tables, and a CPU inference engine.
Rust · Lean 4 · Aeneas · Charon · GGUF -
Research · active
Song
An operating system, language and compiler, with proof responsibility down to native instructions and bytes.
Iota · x86-64 · Lean 4 -
Research · active
Simulation
World generation, physical simulation and game systems on the same algebra.
Rust · Bevy · Luau
Writing
All writing →-
The charter, costed and scheduled
The full Sanguine Host charter: nineteen core policies, two candidates, a justice system, a rights floor, costs, sequencing and the first 100 days.
-
From borrowing to bytes
Memory safety from Rust borrowing to native-code verification. Song's first x86-64 multiplication has a Lean proof; the full compiler and kernel are ahead.
-
One multiplication, three geometries
Complex, dual and split-complex numbers through one multiplication rule. Interactive figures show rotations, shears and squeezes, with links to Lean proofs.
The dial
How it works →- face
- elliptic
- σ
- −1.000
- flow(σ, t)
- 0.622 + 0.783·x
- N
- 1.000