PERSONAL PROJECT / LOGIC · MATHEMATICS · STEM

ProofGym

AI can give you an answer in seconds. ProofGym gives you a reason to work through one yourself. Build logical arguments step by step and tackle STEM problems that ask you to question assumptions, connect ideas, and explain why a conclusion follows. The goal is to keep deep, independent thinking in practice.

React · TypeScriptFormula parserProof validationZustand
Try the live application

PROJECT EXPLORER

Explore ProofGym with AI

AI can supply an answer. ProofGym asks you to build the reasoning. Explore why this project exists, how its logic and STEM exercises work, or the code behind them.

View code · ProofGym · lib/validator.ts · isAccessible
export function isAccessible(
  targetId: number,
  fromId: number,
  allLines: ProofLine[],
  closedSubproofs: ClosedSubproof[],
): boolean {
  if (targetId >= fromId) return false

  const targetLine = allLines.find(l => l.id === targetId)
  if (!targetLine) return false

  // A closed subproof's interior is inaccessible to lines OUTSIDE it.
  // Lines inside the same subproof can still reference each other freely.
  for (const sp of closedSubproofs) {
    if (targetId >= sp.startId && targetId <= sp.endId) {
      // Target is inside this closed subproof.
      // Only inaccessible if fromId is OUTSIDE the same subproof.
      const fromIsInside = fromId >= sp.startId && fromId <= sp.endId
      if (!fromIsInside) return false
    }
  }
  return true
}

AI guide to this project. Questions are processed by OpenAI.

TRY A SMALL ARGUMENT

Don’t just accept the conclusion.
Follow the reasoning.

A Fitch proof is an argument written one justified line at a time. Indentation marks a temporary assumption; rule names and line numbers show exactly why each new statement follows.

PROVE P → R

P · practiceQ · improveR · harder problems

2/6 lines

A small propositional-logic example, created for this portfolio. ProofGym lets you construct your own proofs and practice with logic, STEM, and critical-thinking challenges.

WHY I BUILT IT

A Place to Practice Thinking Deeply

I built ProofGym as a place to practice independent reasoning in an age of instant answers. Explore a problem, examine its assumptions, and build an argument you understand one step at a time.

DESIGN DECISIONS

How the pieces fit.

  • Parse formulas into a structured syntax tree before comparing them.
  • Separate proof state and validation from the React interface with Zustand.
  • Reuse the proof workspace for curated, generated, and custom exercises.

ENGINEERING FOCUS

A TypeScript formula parser, rule-specific validation, nested subproof scope, and a procedural exercise generator sit behind the interactive workspace.

CONTEXT & SCOPE

A browser-based personal project built with Next.js, React, TypeScript, Zustand, Tailwind CSS, and KaTeX. Progress is saved locally in the browser; accounts and cloud synchronization are not part of the inspected implementation.

INSIDE THE IMPLEMENTATION

From a formula to useful feedback.

A typed logic engine supports the interface, while separate stores handle the current proof and saved progress.

1. Parse the input

Normalize typed symbols, tokenize the formula, and build a syntax tree with operator precedence. Structural comparison checks formulas beyond their raw text.

2. Check the step

Validate the chosen rule and cited formulas. Scope checks prevent a step from borrowing a line inside a subproof that has already closed.

3. Update the workspace

Zustand tracks proof lines, open assumptions, closed subproofs, hints, and undo. React presents the proof and validation feedback.

4. Keep practice varied

A backward-construction generator builds exercise candidates with difficulty tiers and hints. Browser-local progress tracks solved exercises, XP, medals, and streaks.

The STEM arena includes logic, mathematics, critical thinking, physics, biology, and chemistry. Logic puzzles can reuse the same proof workspace.