Starscape

Eye standing

W A S D or arrows walk · drag the ground to pull the world · right-drag to look

Stars Stars drawn as Brightness exponent β 0.55 Colors

|Δ| = 3240

two real rootsdouble rootlower cone

Brightness Star size Light cone Dust outside the cone Lower cone Multiples (non-primitive forms) Reduce motion

Drag to orbit. Scroll or pinch to zoom. Right-drag or two fingers to pan.
At the origin: drag the sky to move every star by a Möbius map. Right-drag or two fingers to look around. W A S D lean your eye off the origin.
Tap a star to read its polynomial. Shift-tap a second star for the geodesic through both.
← → chapters · O outside/origin · P next picture · T S symmetries · Esc clear

In Lean 4: the identities behind the lattice, its symmetry and the necklaces, kernel-checked; counts and class numbers as compiled tests; and the exact data this page is tested against.
On FloatLib: a proof that the GPU’s float32 arithmetic marks shells and necklaces exactly.
lean-starscape: the same sky driven by a live Lean service, with browser, WebXR and visionOS renderers.
The guide: how this page is built, with the derivations.

This is an independent implementation inspired by Katherine E. Stange’s Starscape / Lattice viewer and her talk Illustrating Mathematics. The mathematics is from Edmund Harriss, Katherine E. Stange and Steve Trettel, Algebraic Number Starscapes (§4.2). The left/right coding of geodesics in the companion Farey view is due to Caroline Series, The Modular Surface and Continued Fractions (1985).

Built by Alok Singh with AI collaborators. No code or media from the original viewer is included. Source