Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 1 result · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Nelson–Aalen, Kaplan–Meier, Greenwood — Examples

1 · Prerequisites

2 · Summary

The hand calculation follows two failures through their risk sets, computes the Nelson–Aalen and product-limit estimates, and evaluates Greenwood's formula where its denominators are positive. Two event-time laws produce exactly the same data under a fixed censoring horizon while having different survival tails, showing why estimates beyond adequate follow-up are not identified by the observed law.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

A hand Kaplan–Meier calculation and loss of tail support

Example

The observed right-censored sample has failures at times $1$ and $2$ , followed by two censorings at time $3$ : $(U_{i}, δ_{i}) = (1, 1), (2, 1), (3, 0), (3, 0)$ . Consider also two possible IID event-time laws with deterministic censoring at $C_{i} = 3$ : under law $P_{A}$ , $P (T_{i} = 1) = 1 / 4$ , $P (T_{i} = 2) = 1 / 4$ , and $P (T_{i} = 4) = 1 / 2$ ; under law $P_{B}$ , the first two probabilities are the same and $P (T_{i} = 5) = 1 / 2$ .

Facts & Assumptions

Given: The four observed records above and the two candidate event-time/censoring laws.

[F1]

Right censoring records $U_{i} = \min (T_{i}, C_{i})$ and $δ_{i} = 1 {T_{i} \leq C_{i}}$ , so a tie at the censoring time is recorded as an event. (Event-time observation, censoring, and truncation schemes)

[F2]

Nelson–Aalen uses each event count divided by its risk-set size over $[0, t]$ , Kaplan–Meier multiplies the factors $1 - d_{j} / Y_{j}$ over event times in $[0, t]$ , and Greenwood uses ${\hat{S}}^{2} \sum_{j} d_{j} / [Y_{j} (Y_{j} - d_{j})]$ only when the event denominators are positive. (Nelson–Aalen, Kaplan–Meier, and Greenwood estimators)

[A1]

Censoring is deterministic at time $3$ under both candidate laws, so $T_{i}$ and $C_{i}$ are independent.

Verification

1.1F2givenalgebra

At time $1$ , all four subjects are at risk and one fails, so $Y_{1} = 4, d_{1} = 1$ . At time $2$ , three remain at risk and one fails, so $Y_{2} = 3, d_{2} = 1$ . By [F2], ${\hat{Λ}}_{n} (3) = 1 / 4 + 1 / 3 = 7 / 12$ and ${\hat{S}}_{n} (3) = (1 - 1 / 4) (1 - 1 / 3) = 1 / 2$ .

2.1F2step 1.1algebra

Both Greenwood denominators are positive, and [F2] gives ${\hat{V}}_{G} (3) = \frac{1}{4} (\frac{1}{4 \cdot 3} + \frac{1}{3 \cdot 2}) = 1 / 16$ . The two censorings at time $3$ add no event increment, so all three estimates remain at these values after time $3$ if the product and sum are carried forward.

3.1A1F1algebra∎

Under either law in [A1], an event time above $3$ produces the same observed record $(U, δ) = (3, 0)$ ; event times $1$ and $2$ produce $(1, 1)$ and $(2, 1)$ . Thus the entire observed-data law is identical under $P_{A}$ and $P_{B}$ , while $P_{A} (T > 4.5) = 0$ and $P_{B} (T > 4.5) = 1 / 2$ . Survival beyond the censoring horizon is therefore not identified by these observations.