Discrete Math Proof Assistance Evals

This project is an empirical study of how well modern AI assistants help a student work through discrete-math proofs.

The goal is not to rank models by raw problem-solving ability. The goal is to measure whether a model can help a student make valid proof progress while preserving student agency.

Research Questions

1. How do frontier models differ when tutoring proof construction? Which models diagnose proof errors, choose useful hints, and keep the student doing the work?

2. Where do models over-help or under-help? When do they write the proof for the student, give vague encouragement, or miss a mathematical mistake?

3. How reliable is automated scoring for proof-tutoring quality? Where does an LLM judge agree with human scores, and where does it miss mathematical or pedagogical issues?

Proof writing is a high-friction learning goal in discrete mathematics. A useful AI tutor should notice invalid algebra, prompt the student toward definitions, and preserve the learning task. A weak tutor may silently validate a bad proof or produce a polished final answer that bypasses the student's reasoning.

Evaluation Design

This v1 uses scripted multi-turn conversations. Each task has:

• a synthetic proof problem adapted from core discrete-math proof topics
• three fixed student turns
• one or more intentional student mistakes or pressure moves
• private reference notes used only for scoring

The evaluated model sees the problem statement and scripted student messages. It does not see the reference proof skeleton, common misconceptions, or red-flag failures.

For the full methodology, task map, and scoring rubric, read the Evaluation Design.

The first version covers:

• direct proof
• parity and cases
• contradiction
• contrapositive
• induction
• set inclusion and set equality
• prove/disprove reasoning
• academic-integrity pressure inside a proof workflow

What You Will Produce

• JSON and Markdown transcripts for each model/task conversation
• human rubric scores for each transcript
• automated judge scores for comparison
• Markdown analysis tables
• a RESEARCH_LOG.md documenting hypotheses and decisions
• a FINDINGS.md writeup with recurring failure modes and judge limitations

A successful v1 produces 60 model transcripts if you run the six configured models across all 10 tasks, complete human scores for every transcript, judge scores after human scoring, agreement analysis, and at least three recurring proof-tutoring failure modes with transcript evidence.

Implementation Work

The repo has three incomplete scripts. Work through these guides in order:

Before editing code, complete Setup. After the scripts work, follow Research Workflow and Follow-Up for the study sequence.

Guardrails

• Do not give evaluated models the contents of reference_keys.json.
• Do not edit raw transcripts after generation.
• Do not run the LLM judge before writing human scores.
• Do not treat the aggregate score as the whole result; qualitative failure modes matter.
• Record exact model IDs and run dates in FINDINGS.md.
• Use dry-run and stub modes before spending API calls.