Revision #3639 → #4181 · back to history
modifiedBellman equation (lead)81198c547851
| Field | From #3639 | To #4181 |
|---|
| note | No declaration referencing the Bellman equation was found in Mathlib. | Grep of Mathlib for `Bellman` returned no files. |
modifiedHamilton–Jacobi–Bellman equation80ab2c5eb2ca
| Field | From #3639 | To #4181 |
|---|
| note | No HJB equation is present in Mathlib (grep for Hamilton-Jacobi returned no files). | No HJB equation is present in Mathlib (grep for Bellman returned no files). |
modifiedFibonacci overlapping subproblemsf95fa0ccc7b0
| Field | From #3639 | To #4181 |
|---|
| note | `Nat.fib` defines the Fibonacci sequence with the standard recurrence, but the DP/overlap analysis itself is not formalized. | `Nat.fib` (verified) defines the Fibonacci sequence with the standard recurrence, but the DP/overlap analysis itself is not formalized. |
modifiedDijkstra as DPa7dea0c85e71
| Field | From #3639 | To #4181 |
|---|
| note | Dijkstra's algorithm is not present in Mathlib (grep returned no files). | Dijkstra's algorithm is not present in Mathlib (grep for Dijkstra returned no files). |
modifiedSequence alignment problem838737b0af4e
| Field | From #3639 | To #4181 |
|---|
| note | Edit distance / sequence alignment is not present in Mathlib (no Levenshtein decl found). | Edit distance / sequence alignment is not present in Mathlib (grep for Levenshtein/editDistance returned no files). |
modifiedTower of Hanoi puzzlefad248c3ee1a
| Field | From #3639 | To #4181 |
|---|
| note | Tower of Hanoi is not formalized in Mathlib (grep returned no files). | Tower of Hanoi is not formalized in Mathlib (grep for Hanoi returned no files). |
modifiedMatrix multiplication associativityc306dad29519
| Field | From #3639 | To #4181 |
|---|
| note | Associativity (and non-commutativity in general) of matrix multiplication is standard Mathlib content via `Matrix.mul_assoc`. | Associativity of matrix multiplication is standard Mathlib content via `Matrix.mul_assoc` (verified via decl_exists). |