Revision #1694 → #2437 · back to history
e7404f1e8c45| Field | From #1694 | To #2437 |
|---|---|---|
| note | The statement `E[X] = pn` is declared in Mathlib as an unproven `proof_wanted`, so it is not yet actually formalized. | The statement `E[X] = pn` is declared in Mathlib as an unproven `proof_wanted`, so it is not yet actually formalized. (Mathlib declares this as `proof_wanted` — stated, not yet proven.) |
| provenance | ai | ai-moderated |
| status | partial | not_formalized |
e2f53a17cf23| Field | From #1694 | To #2437 |
|---|---|---|
| note | The statement `Var[X] = p(1-p)n` exists only as an unproven `proof_wanted` declaration. | The statement `Var[X] = p(1-p)n` exists only as an unproven `proof_wanted` declaration. (Mathlib declares this as `proof_wanted` — stated, not yet proven.) |
| provenance | ai | ai-moderated |
| status | partial | not_formalized |