Attempt · sample contribution
Apply the witness at the original bound
The non-strict witness gives n ≤ p, which cannot establish n < p.
Lean typecheck failed
Approach
Applying the pinned theorem at n yields only a prime at or above n. This failure remains available as prior work for the next attempt.
Open the context used →Observed Lean run
The attempt records the work; the run records what happened when its file was checked.
Off-by-one proof attempt fails
hbound has type n ≤ p but is expected to have type n < p
What carries forward
The starting and updated context packs both retain this failure, so another contributor can see the obstruction.
Open starting context →