Skip to content

Docs: dated current-routing clarification in formal verification guide #393

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
d6g8k5htny-coder merged 3 commits into from
Oct 14, 2026
Merged

Docs: dated current-routing clarification in formal verification guide #393

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d7bebec
Clarify current formal-guide claim route; preserve September pilot hi…
d6g8k5htny-coder Oct 7, 2026
cb42f6b
Update current-routing note to main#307 (successor board); preserve h…
d6g8k5htny-coder Oct 13, 2026
f84dc39
Merge branch 'main' into grok/formal-guide-routing-20261007
d6g8k5htny-coder Oct 14, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 17 additions & 2 deletions docs/FORMAL_VERIFICATION.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,19 @@

Owner directive: Dylan Roy, 27 September 2026. Scientific effect: **NONE**.

## Current routing (13 October 2026)

This dated note is contributor routing only. It does not change formal source, the required-check contract, branch protection, or any scientific disposition. A merge or green check is not theorem acceptance.

New formal work is claimed on the relevant current formal pull request, not on closed [main#95](https://github.com/d6g8k5htny-coder/main/issues/95). Use [main#275](https://github.com/d6g8k5htny-coder/main/issues/275) and [main#307](https://github.com/d6g8k5htny-coder/main/issues/307) for discovery and coordination. Read the current workflow before writing, and reconcile exact-path ownership with any open documentation lane.

Later formal companions, kept distinct from the September scalar pilot:

- Landed cap companion: [Math- `frontiers/cap_first_exit_lean_20261002/README.md` at `7d2f62500ad6effba2bbdf6f3b89b0826408dc4a`](https://github.com/d6g8k5htny-coder/Math-/blob/7d2f62500ad6effba2bbdf6f3b89b0826408dc4a/frontiers/cap_first_exit_lean_20261002/README.md) (README blob `4f5e1bf09f3ae7acf8dc60289697f40baecba56c`, as cited by main#286). This is a conditional deterministic formal companion, not kernel evidence for the full probability or persistence-module theorem.
- Retained formal interfaces: [Math-#193](https://github.com/d6g8k5htny-coder/Math-/issues/193).

The September pilot history below, including its original source identities and failed hosted build, stays unchanged as historical evidence.

This extends the existing [formal-ladder work item #95](https://github.com/d6g8k5htny-coder/main/issues/95). It does not renumber that ladder, replace the scientific-status authority, or retroactively describe reviewed informal proofs as formal proofs.

## One proof, several separate questions
Expand All @@ -16,7 +29,7 @@ This extends the existing [formal-ladder work item #95](https://github.com/d6g8k

The primary backend is Lean 4 + mathlib. Dependencies and workflow actions are pinned. Formal evidence is an additional conjunction in a future promotion decision, never a substitute for a missing parent obligation. The present pilot does not change repository-wide branch protection or the controlling promotion engine.

## Implemented pilot and exact sources
## Implemented pilot and exact sources (historical, September 2026)

[Math- PR92](https://github.com/d6g8k5htny-coder/Math-/pull/92) introduces an isolated `formal/` package. Inspect the exact successor [commit cc2989c1280f4f227d0c6aa30c8841d6ba01e46e](https://github.com/d6g8k5htny-coder/Math-/tree/cc2989c1280f4f227d0c6aa30c8841d6ba01e46e/formal) and its [execution run](https://github.com/d6g8k5htny-coder/Math-/actions/runs/36352398376). A PR link is not evidence that it has landed; the run itself supplies its outcome.

Expand All @@ -34,7 +47,9 @@ The controls include false fold and power inequalities, a `sorry` proof, an indi

`none`, `specified`, `proved` (proof text supplied), and `kernel-checked` are formal-progress labels. Independent alignment is a separate pending/accepted/stale dimension. None is a replacement for scientific ACCEPT/AMEND. An authenticated alignment review must bind the exact manifest, scope and complete target set, cite immutable review evidence, and record different author/reviewer provider, family and agent. A validator checks that contract; strings alone cannot authenticate a reviewer.

## Standing instructions for current and future agents
## Historical standing instructions (September 2026 pilot)

The following offer table is retained as the September pilot record. It is not the current claim route. Current claim route: the relevant open formal pull request, with discovery and coordination on main#275 and main#307. Closed #95 and Math- PR92 remain the historical pilot references used to avoid rewriting that record.

Use #95 and PR92 to claim work and avoid duplicate writers. The OpenAI implementation author does not supply independent review credit. Read the exact head before reviewing; changed source, scope or dependencies invalidate the prior alignment record.

Expand Down
Loading