Attempt · sample contribution
Shift the bound by one
Apply the pinned theorem at n + 1 and derive a strict bound.
Lean typecheck passed
Approach
Applying the pinned theorem at n + 1 yields a prime above n. The attempt records this route against a specific starting context.
Open the context used →Observed Lean run
The attempt records the work; the run records what happened when its file was checked.
What carries forward
The updated context pack includes this passing local run alongside the earlier failed route.
Open updated context →