Two finite cases make the idea tangible. These are model results and operation counts—not elapsed-time, token or monetary savings.
02 / Scheduling5 jobs · 2 workers
A good order isn’t always the best.
The same five jobs. The same two workers. A different assignment closes a one-unit gap.
7time units List-schedule makespanLower bound: 6
The model. Independent, non-preemptive jobs of lengths 3, 3, 2, 2, 2; two identical workers; all available at time zero. Total work is 12, so every schedule takes at least 6 units. The exact assignment reaches 6, proving optimality for this instance.
Approved example reference · beff82f3814f
03 / Result reuse256 accepted tasks
An unchanged result stays useful.
Once the complete task graph is indexed and its tasks accepted, repeated graph traversal can fall away.
0repeated node visits
0dependency reads
256membership hashes remain
The case. A complete 256-task DAG, already indexed, all tasks accepted and relevant inputs unchanged. Indexed reuse avoids 512 repeated node visits and 32,640 dependency reads. It does not eliminate the 256 membership hashes or the initial indexing work.
Approved example reference · beff82f3814f
Illustrations, not live telemetry. Counts belong to the stated cases; they are not a general performance guarantee.
The approach
Structure you can build on.
Optimal is a toolkit for developers building agent teams. The aim is deliberate work, with dependencies and evidence close at hand.
Declare the relationships.
Explicit dependencies and contracts make it possible to reason about which work is affected—and which work is not.
Keep useful results.
Versioned results and scoped checks keep reuse tied to the relevant inputs. Unchanged does not have to mean recomputed.
Make the boundary visible.
Formal reasoning is useful when its assumptions are explicit. A proof about a model is not a promise about every implementation.
Proof & its boundaries
Proofs with explicit premises.
Scoped Lean proofs make the model and its assumptions explicit. The finite examples here show where a result can be established and where further evidence is needed.
01The premises matter.
The scheduling result assumes the five declared job lengths and two identical workers. Reuse assumes a complete, already-indexed graph, accepted tasks and unchanged relevant inputs.
02A model is not the running system.
Lean checks formal statements within their definitions and assumptions. Correspondence with production code, dependency completeness and real-world inputs needs separate justification.
03Counts are not clocks.
Fewer graph operations do not by themselves establish lower latency, fewer tokens or lower cost. No general scheduling optimality or end-to-end performance guarantee is claimed.
Evidence scope: the finite examples above. The diagrams explain the relationships; they do not run experiments or verify proofs in your browser.
Current status
Built carefully. Still in development.
Optimal is in private development. This public preview shares the approach, finite examples, and the boundaries of the available evidence.
Research direction / not a current capability
Derive more. Assume less.
Automated dependency derivation and machine-learning-assisted approaches are proposed future work. They are not established capabilities or evidence behind the results shown here.
