Inspiration
We unit-test code before trusting it. Why don't we unit-test understanding?
Most AI tutors wait for a wrong answer and then explain the right one. But one hidden rule—“a larger denominator means a larger fraction,” for example—can generate ten future mistakes. We wanted a tool that tests the mental model itself.
What it does
Invariant converts a learner's plain-language belief into a safe executable hypothesis. The learner first approves what Invariant thinks they mean. A deterministic verifier then searches real cases, ranks failures by simplicity, and presents the smallest counterexample as a certificate.
The flagship fractions flow turns “A fraction with a larger denominator is larger” into an explicit claim and finds 1/3 < 1/2. Equal-width fraction bars make the contradiction impossible to hand-wave away. The learner patches the rule, retests it, and answers a transfer question about pizza slices.
Invariant also includes linear-functions and probability packs. It can disprove “the line with the larger slope is always above” with a graph and witness point, and it separates exact 50/50 coin probability from a seeded simulation when confronting the gambler's fallacy.
How we built it
Invariant is a strict TypeScript application using Next.js App Router, React, Tailwind CSS, Zod, Lucide icons, and lightweight custom SVG visualizations.
The optional AI layer uses the official OpenAI JavaScript SDK against Featherless's OpenAI-compatible API. The model acts only as a semantic compiler: it maps wording into a constrained HypothesisSpec AST. Every response is parsed and validated with Zod; malformed output is retried once and then routed to a deterministic pack-specific fallback.
Mathematical truth stays outside the model. A recursive evaluator safely executes the AST without eval. Concept-pack verifiers enumerate valid assignments in deterministic order, evaluate assumptions and claims, score failures for simplicity, and return the smallest witness. Supported repaired rules may use exact pack-specific checks; all other no-failure results retain an explicit bounded-search limitation.
Challenges we ran into
The hardest design problem was maintaining a clean trust boundary. A fluent explanation is not mathematical evidence, so the language model could not be allowed to invent test results. We also had to make counterexample selection feel immediate without faking activity, keep three mathematical domains behind one plugin contract, and distinguish “survived these tests” from “proved.”
Another challenge was visual compression. The entire compile → attack → repair story needed to remain legible in a sub-two-minute demo and on a 1440×900 recording, while still providing enough assumptions and provenance for the result to be auditable.
Accomplishments we are proud of
- A genuinely different educational interaction: testing beliefs rather than generating answers.
- A safe serializable AST with no dynamic code execution.
- Real deterministic search, deterministic tie-breaking, and smallest-witness certificates.
- An offline-complete flagship flow that does not pretend a fallback is AI.
- Three domain visualizers built without a heavy charting dependency.
- Honest epistemic labels for counterexamples, bounded survival, and supported exact rules.
- A repair-and-transfer loop that measures whether the learner changed the rule, not just whether they saw an explanation.
What we learned
Counterexamples are unusually efficient teaching objects: one small witness can do more conceptual work than a paragraph of correction. We also learned that AI becomes more trustworthy when its role is narrowed. Here it is valuable at translation, while deterministic code remains valuable at verification.
Finally, educational confidence and mathematical confidence are different. A learner's “How sure are you?” rating creates a useful moment of reflection, but it never changes the verifier's result.
What is next for Invariant
Next we would add teacher-authored concept packs, geometry and algebra domains, classroom misconception analytics, and privacy-preserving longitudinal repair history. We would also evaluate whether learners who repair a rule in Invariant outperform explanation-only learners on delayed transfer questions.
Built With
- next.js
- openai
- react
- typescript
- zod
Log in or sign up for Devpost to join the conversation.