This is an explicit beginner project connecting Mathlib with the L-functions and Modular Forms Database. The predicate is elementary and the requested API and examples are enumerated, while acceptance has a concrete Mathlib/LMFDB/LeanBridge path.
formalizationOn hold after campaign review
Formalize totally positive elements of number fields for the Lean-LMFDB bridge
Define `IsTotallyPositive (x : K)` for a number field as positivity under every real embedding, prove closure under addition and multiplication, prove the nonzero-square fact over totally real fields, and add the issue's Q(sqrt 2) examples, following the existing infinite-places API.
The declarations and examples must typecheck against the pinned Mathlib dependency, pass `lake build` and the blueprint declaration checker, and use no `sorry` or new axioms.
- Difficulty
- 4/10
- Attempts
- 0
- Last attempt
- Not yet
- Source status
- open
- External validation
- none
Lean 4number fieldsreal embeddingsordered fieldsLMFDB
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.