Lucas Rose-Winters

Security engineer, now in full-time research and development: an algebra library with Lean refinements, an operating system built up from assembly, and simulation and games on the same basis.

Launceston, TasmaniaResearch & development

Illustrated portrait of Lucas Rose-Winters

Work

All work →

Research · active
Apeiron

A Rust library on ℝ[x]/(x² − σ) and one table, with Lean refinements for its primitives.
Rust · Lean 4 · Aeneas · Charon · GGUF
Research · active
Song

An operating system, language and compiler, bootstrapped from a pinned assembly seed.
Slang · x86-64 assembly · Lean 4
Research · active
Simulation

World generation, physical simulation and game systems on the same algebra.
Rust · Bevy · Luau

Writing

All writing →

28 Sept 2026 One multiplication, three geometries
From nothing to one combinator, to counting, numbers and the plane; then the algebra ℝ[x]/(x² − σ), its three faces and their flow, and why a bounded algebra matters for security, physics and AI.
- algebra
- design
- verification
- ai

The dial

How it works →

face: elliptic
σ: −1.000
flow(σ, t): 0.622 + 0.783·x
N: 1.000

N = 1 (gold), N = 0 away from the origin (red, dashed), and flow(σ, t) from 1 (point). The flow is periodic iff σ < 0.

Lucas Rose-WintersLucasRose-Winters

Work

Apeiron

Song

Simulation

Writing

The dial

Lucas Rose-Winters