A record of every feature, tweak, correction, and design decision across igem-puzzle-v0.1.html through igem-puzzle-v0.42.html, with each one attributed to whoever actually initiated it in conversation — the human user or Claude Sonnet 5.
A change is marked User when the human explicitly requested it, reported a bug, or made an explicit choice between options. It's marked Claude when Claude proposed a design, discovered an issue through its own testing or source inspection, or made an implementation/scoping decision not explicitly dictated. Many changes are genuinely collaborative — e.g. the user asks a feasibility question, Claude proposes a concrete design, the user approves or picks between options Claude laid out. In those cases each *distinct* sub-decision is attributed separately (the question, the proposal, and the approval each get their own row) rather than collapsing the whole exchange into one attribution, so the back-and-forth stays visible rather than flattened.
| Initiated by | Change |
|---|---|
| User | Build a page using Tau Prolog, ramo, and microKanren to solve a specific Einstein/zebra-style puzzle Initial request, including the constraint of minimal original code with textbook-parallel notes for anything unavoidable. |
| User | Supplied the 21-clue puzzle itself, with a claimed unique solution User stated they had already run it through a solver and confirmed one solution. |
| Claude | Independently re-verified the puzzle with a real solver before building anything Not asked for explicitly — done proactively rather than trusting the user's claim at face value. |
| Claude | Discovered the 20-clue version actually had two valid solutions (Ecoplaster/algae ambiguity) Found via exhaustive solving (findall + count), not by inspection. |
| Claude | Proposed adding clue 21 to resolve the ambiguity Suggested exact wording and verified it restored uniqueness. |
| User | Approved adding clue 21 “yes, add clue 21.” |
| User | Reported a console error: ramo failed to load from CDN “Uncaught ReferenceError: ramo is not defined.” |
| Claude | Diagnosed the CDN issue and vendored all three libraries directly into the page instead Removed the external-network dependency entirely; verified byte-identical to the pristine npm packages. |
| Initiated by | Change |
|---|---|
| User | Requested a Tau-Prolog-only version with a debugger and human-readable trace, kept distinct from v0.1 Explicit request to preserve v0.1 unmodified under its own filename. |
| Claude | Discovered Tau Prolog ships an internal, undocumented debugger hook (thread.debugger / debugger_states) Found by reading the vendored source directly rather than assuming a mechanism existed. |
| Claude | Refactored the Prolog program into one named predicate per clue Done specifically so the raw resolution trace had clean, filterable checkpoints — changes nothing about how the puzzle solves. |
| User | Requested a standalone HTML provenance page (not .md), separating Claude-authored code from vendored code, with textbook citations for techniques Explicit request, including the specific example format (“if SICP tells how to do X, note that”). |
| Initiated by | Change |
|---|---|
| User | Requested a second panel showing literal JavaScript code executing, like a real code debugger Explicit request, extending the Prolog-only debugger of v0.2. |
| Claude | Designed the JS panel as independently re-derived checker functions (not mirrored from the Prolog logic), shown via their own toString() and actually executed live Design choice to make the JS panel a genuine second verification rather than a cosmetic display of the same logic twice. |
| Initiated by | Change |
|---|---|
| User | Requested a first-order-logic focus: every clue given in English and in FOL notation, with the solution logged as a step-by-step proof (“21 theorems”) Raised as a feasibility question first (“does that sound reasonable?”), then approved. |
| Claude | Proposed the FOL vocabulary (Country/Organism/Project/Award relations; Succ/Before/Plus3 helpers) Specific predicate/notation scheme proposed as part of answering the feasibility question. |
| Claude | Discovered that four background structural axioms (bijectivity of each relation) were needed for the proof to be well-founded, beyond the 21 numbered clues Flagged as necessary rather than assumed obvious. |
| Initiated by | Change |
|---|---|
| User | Reported that stepping through the trace caused the page to visually jump away from “what's known so far” Described the specific unwanted focus-jumping behavior. |
| User | Requested a specific new layout: known-so-far table leftmost, Play button next to it, proof log to the right, filling in live during Play Explicit layout specification, including that the proof lines should visibly ‘roll in.’ |
| Claude | Diagnosed the root cause as a scrollIntoView() call on the Prolog source pane Traced the jumpy behavior to its exact source before proposing a fix. |
| Claude | Implemented the focal-row layout, removed scrollIntoView, and moved engine internals into a collapsed <details> Implementation of the requested layout plus the underlying fix. |
| Initiated by | Change |
|---|---|
| User | Raised the idea of obfuscating the code so it could be posted publicly without students reading it easily Framed as a “maybe possible” exploratory question. |
| Claude | Pushed back that obfuscation works against the stated pedagogical goal, and proposed alternatives (redaction, predict-then-run, intentional bugs to debug) Reframing based on the clarified goal of getting students to actually engage with the code. |
| User | Proposed that the program should refuse to auto-solve, require dropdown interaction, and offer clues instead of answers Framed as “what if…” design questions. |
| User | Proposed a fixed menu of “possible actions” per clue, some requiring combinations of clues Extension of the above design idea. |
| User | Decided the action menu should show only productive moves, and only suggest combinations known to be useful (beginner-friendly) Explicit answer to Claude's question about scope. |
| Claude | Distinguished “different orderings of one proof” (free) from “structurally independent routes to the same fact” (requires new clues) as two different meanings of “multiple proofs” Conceptual clarification offered before committing to a design direction. |
| User | Requested the richer kind: genuinely independent proof routes, even if it required adding clues Chose between the two options Claude had distinguished. |
| Claude | Proposed and verified clue 22 (Hong Kong = USA + 1) as a second, independent route to Hong Kong's year Verified via the real solver: consistent when added, and independently sufficient with clue 9 removed. |
| User | Raised the bar: wanted three totally distinct proofs from one clue set “It would be very impressive to have a single set of clues that could generate 3 totally distinct proofs.” |
| Claude | Proposed and verified clue 23 (Hong Kong worked with Black Soldier Fly) as a third independent route Verified the same way: independently sufficient with the other two routes removed. |
| User | Specified that once a combination is picked, the resulting formula should be revealed immediately (no extra multiple-choice step) Simplification requested specifically to keep the tool easy for beginners. |
| Initiated by | Change |
|---|---|
| User | Set a 35-minute real-world build budget and asked Claude to start coding Explicit timebox given. |
| Claude | Scoped the build to a fully self-contained page, dropping the v0.3x multi-engine debugger panes to fit the time budget Scoping decision made to deliver a complete, tested artifact within the stated time rather than a partial one. |
| Initiated by | Change |
|---|---|
| User | Reported that clicking clue 2 filled in two table cells, and asked whether that was correct Noticed the discrepancy by testing the tool directly. |
| Claude | Diagnosed this as a real bug: clue 2 only licenses a relative fact (“X is one year after Y”), not an absolute row — that requires a joint case-exhaustion argument across clues 1–5 Explained why the reveal was logically unearned, not just cosmetically wrong. |
| User | Required that the table never be filled in for free — the user must click buttons and see the inference happen, at minimum Explicit requirement set after the bug was identified. |
| Claude | Designed the “Step 2” case-exhaustion tool: four candidate starting years, each individually tested, cells revealed only once all four are tested Concrete fix implementing the user's requirement. |
| Initiated by | Change |
|---|---|
| User | Requested real Fitch-style notation: single uppercase predicate letters, possibly with subscripts Explicit request for a more rigorous, textbook-accurate notation. |
| Claude | Proposed the specific notation (C/O/T/A predicates, year-as-subscript, short constant codes like NEM/CYA/HK) Concrete scheme proposed in response to the notation request. |
| Claude | Raised whether ∀-Elim and Modus Ponens should be collapsed into one line or shown separately Design question posed before committing to an approach. |
| User | Decided they should be two separate lines Explicit choice for full rigor over brevity. |
| Claude | Raised whether reductio arguments should get real nested Fitch subproof boxes Design question posed alongside the ∀-Elim/MP question. |
| User | Decided yes: real Fitch subproof boxes for the reductio arguments Explicit choice for full rigor. |
| Claude | Discovered two more background axiom families were needed for true logical bottom: Unique Names and total order/domain closure on years Identified while working out exactly what each reductio box would need to cite. |
| Claude | Discovered the four candidate-year cases have four genuinely different internal proof shapes, not one reusable template Worked out case-by-case rather than assuming uniformity. |
| User | Confirmed the fully-detailed scope (“aim for maximum granularity”) Approved the depth Claude had proposed after laying out what it would entail. |
| User | Directed Claude to start coding v0.42 “That looks good, you can start coding.” |
| Claude | Found and fixed a real bug during its own testing: clue 23 was missing its hkRoute tag, so it silently re-derived Hong Kong's year via ordinary MP instead of being flagged as the third independent route Caught by Claude's own end-to-end test, not reported by the user. |
| User | Reported confusion: 23/24 facts known, the one remaining clue (9) unused, expecting it would resolve China's missing project cell Described the specific (mistaken) expectation the UI created. |
| Claude | Diagnosed the real issue: the progress text was misleading (23/24 reads as ‘one more to go’); 23 is actually the ceiling, and the unnamed algae project is intentionally unrecoverable from any clue Explained the actual situation and proposed correcting the progress message. |
| User | Reported that the starred (Hong Kong) clue options in “Apply the remaining clues” seemed unusable in their current state Observed the buttons sitting disabled with no explanation. |
| Claude | Diagnosed this as a regression: v0.41's “why not ready” hint text had been silently dropped in v0.42 Identified the missing feature by comparing against the prior version's behavior. |
| Claude | Restored hint text explaining why each disabled clue isn't ready yet Fix for the diagnosed regression. |
| User | Asked whether the interface could be redesigned so the user isn't forced to start from clue 1, while keeping the Fitch proof valid Explicit request questioning the rigidity of the fixed clue order. |
| Claude | Analyzed the real dependency: clue 1 must happen before the case-analysis step (it rules out organism-placement ‘gap’ scenarios), but doesn't need to be clicked first; clues 2–5 have no ordering constraints among themselves Distinguished genuine logical necessity from arbitrary UI sequencing before changing anything. |
| Claude | Implemented five independently-orderable buttons for clues 1–5, unlocking the disjunction only once all five are done, in any order Fix verified with a deliberately scrambled click order (3, 5, 2, 4, 1). |
| User | Requested a live, incremental “plain English” paraphrase panel below the Fitch proof, same line numbers Explicit request for a second, parallel narrative view. |
| Claude | Raised design options: inline vs. separate panel; live vs. one-shot; bespoke vs. simplified prose for the reductio arguments Design questions posed before implementation. |
| User | Chose: separate panel, live/incremental, and simplified reductio phrasing (“by reductio ad absurdum,” no bespoke re-explanation each time) Explicit answers to each of the three design questions. |
| Claude | Implemented the plain-English panel across all 64+ derivation-line call sites, verified zero missed glosses and exact line-number parity with the Fitch panel Implementation plus its own verification pass. |
| Claude | Caught and fixed an awkward sentence in the Hong-Kong-fork English message during its own review Self-caught during a final read-through, not reported by the user. |
| Initiated by | Change |
|---|---|
| User | Requested this provenance/changelog file, explicitly tracking which changes were user-demanded vs. Claude-suggested Current request. |