ASSUMPTION ARCADE makes mathematical assumptions editable so learners can explore where conclusions survive or fail. The local prototype explores equivalence relations and overlapping classes: learners edit a finite relation, remove transitivity, inspect a concrete counterexample, repair relations, and export or reopen a lesson.
A bounded search miss is not a general proof. The JavaScript implementation includes relation checks, repairs and JSON/SVG export; nine tests passed. A direct Nebius/Nemotron-3-Super counterexample request for Rolle’s theorem with differentiability removed returned |x| on [-1,1], accepted by the numerical checker. This does not establish general correctness or learning effectiveness. The video is a narrated saved-screenshot walkthrough, not a live interaction.

Log in or sign up for Devpost to join the conversation.