Implication notes
What is not a checked implication: attempts that established nothing, derivations rejected as routine, and the curated suggestions still without a Lean check. None of it is a claim; nothing here says an implication is false.
Unresolved attempts (3719)
No derivation within the rules and depth, a time or heartbeat limit reached, or an environment that would not import. A limit reached means not established, never false.
| status | reason | attempts |
|---|---|---|
| no-proof | no derivation within the rules and depth | 2851 |
| no-proof | the first source's conclusion supplies no hypothesis of the second | 577 |
| budget | norm_num reached its heartbeat limit | 123 |
| error | universe levels are not determined | 67 |
| budget | wall-clock limit of 10000 ms | 50 |
| error | unknown free variable `_fvar.…` | 20 |
| budget | (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has bee | 14 |
| budget | (deterministic) timeout at `isDefEq`, maximum number of heartbeats (200000) has | 7 |
| audit-failed | uses axioms outside the allowed set | 6 |
| budget | maximum recursion depth has been reached use `set_option maxRecDepth <num>` to i | 4 |
Rejected derivations (4)
Lean checked these, but they are not counted: a source the derivation does not use, or a statement that holds without any source.
- a source is unused: 2
- holds without the sources: 2
Every attempt, with its reason and cost, is in the catalogue data: the index and its shards.
Candidates
- fluid-halting-with-single-fold: Fluid halting detection plus single-fold representation