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.
PERSONAL PROJECT / LOGIC · MATHEMATICS · STEM
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.
Try the live applicationTRY A SMALL ARGUMENT
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.
P · practiceQ · improveR · harder problems
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
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
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
A typed logic engine supports the interface, while separate stores handle the current proof and saved progress.
Normalize typed symbols, tokenize the formula, and build a syntax tree with operator precedence. Structural comparison checks formulas beyond their raw text.
Validate the chosen rule and cited formulas. Scope checks prevent a step from borrowing a line inside a subproof that has already closed.
Zustand tracks proof lines, open assumptions, closed subproofs, hints, and undo. React presents the proof and validation feedback.
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.