Theoremcore
Optimality of A*
Also called A* optimality theorem.
With an admissible heuristic, A* returns an optimal solution; with a consistent one, no node is expanded twice.
With an admissible heuristic, A* returns an optimal solution; with a consistent one, no node is expanded twice.
About this page
The build computes these levels from the evidence in the repository. Each row says what the next level needs. Read what the levels mean.
| Ladder | Level | What the next level needs |
|---|---|---|
| Human proof | H0 no proof |
|
| Lean | L0 no Lean part |
|
| Visual | V0 none |
|
| Writing | W0 stub |
|
Tag QFQ6NX Edit this page History Report an error