Repository navigation
Add visual manual and organize Proof Atlas in the site's scientific style - #127
Merged
Merged
Conversation
moiseevigor
marked this pull request as ready for review
October 24, 2026 18:40
moiseevigor
changed the base branch from
feat/proof-atlas-free-index-multiplicity
to
master
October 24, 2026 18:40
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Proof Atlas mixed a separate green palette, a scattered constructor reference and a long chronological implementation record. This change gives it the blog's scientific article styling and one reading route: notation → compiled proof explorer → research program. Detailed checks are searchable in a separate evidence index. The Projects list becomes a borderless editorial list.
The new visual manual covers all 12 Expr forms and 27 semantic fields, lexical scope, sharing, exact cuts, folding, typed construction schemata and universe/source boundaries. Its four interactive controls use the production scene model and explicitly have no native typing certificate. The older constructor gallery now preserves every semantic field, including all three
letEchildren.The manual, grammar, readers and canvases share Source Serif 4, IBM Plex Sans, IBM Plex Mono and the site theme tokens. Eight manual rules use the existing KaTeX renderer. Canvas themes update live without changing source selections; relation labels, line styles and glyphs remain explicit. The Projects list removes repeated separators, badges and the third-party button widget.
The canonical program retains its goal and representation contract, with a short reading route, capability table and open questions. All 63 former technical sections are preserved verbatim, grouped into five research layers. All 75 old section anchors remain available; old program fragment links forward to the preserved evidence sections. The published research post and mathematical manuscript source are unchanged.
Validation:
f467d72dbda2e3f853c9dcd69715ee37f41b8e55ac192db87162fd59213ba2f7.No compiled proof packet, native query, original Lean source, mathematical article or blog post is changed. This establishes presentation/navigation fidelity, not improved proof comprehension or a completed semantic language.
Depends on the compiled-count release in #126, now merged. The final navigation regressions cover the four-entry Projects list, ordered Atlas route, legacy evidence redirects, keyboard scrolling of retained rules and universe controls (including corrupt/missing optional fixtures).
The shared theme preserves the existing 44-pixel interaction targets in context-accounting, context-interface, scope and witness controls. The full browser regression caught a more-specific theme rule reducing those targets; the fix retains the existing assertions.
Deployed in merge
0d991e84b88b657935db8568bd68703bedde6c79after all seven exact-head checks passed. The actual merge tree matches the tested tree. Pages deployment succeeded for that merge.Hosted verification passed all 14 browser suites and compared all 4,252 updated count/runtime assets byte-for-byte with the tested release. This includes 269 syntax-count frames / 1,430 annotations, 84 article path bridges, desktop/phone and both-theme checks.
Live: Proof Atlas · Visual manual · Projects.