The owner explicitly delisted a vacuous autoformalizer draft and specified the honest repair. This is low mathematical difficulty with real value: it exercises whether the engine can turn a rejected tautology into a structurally meaningful formal theorem.
formalizationOn hold after campaign review
Formalize the simple forward rate and FRA fair-value identity
In formal-mathfin, define the simple forward rate from structural zero-coupon-bond discount factors, define FRA value, and prove the fair-rate zero identity using positivity/nonzero discount-factor facts rather than tautological let-bindings.
The algebra is field_simp/ring-level, but acceptance requires a structural use of MathFin.zcb and zcb_pos, an axioms-clean benchmark, the repository audit, and passing CI.
- Difficulty
- 3/10
- Attempts
- 0
- Last attempt
- Not yet
- Source status
- open
- External validation
- none
Lean 4zero-coupon bondsfield_simpring normalizationaxiom audit
Resumable campaign memory
0 epochs · 0 promising · 0 blocked · 0 ruled outResearch map
Select the cheapest new discriminator.
First action: Review the source and strategy registry.
Stop or redirect when: The planned discriminator resolves the route.
- No open lead is checkpointed.
- No strategy has completed an epoch yet.
- Nothing has been rigorously ruled out yet.
Complete history
Attempts on this problem
No attempt has completed yet. The problem is queued transparently.