There are six possible edges on four labeled vertices, so every simple graph on those vertices can be encoded by six binary choices. An exhaustive search therefore has 2⁶=64 cases. A computer can check all of them quickly, but the mathematical claim still needs an encoding argument and a correct property checker.
Compare this finite claim with “the property holds for every finite graph.” Testing 64 cases covers one order, not all orders.
Predict
Suppose a program reports that every graph in its list satisfies a property. What could be wrong even if every reported line looks plausible? Consider omitted encodings, duplicated cases, a mistaken checker and arithmetic approximations separately.
Experiment
Use a small exact claim: every simple graph on three vertices has degree sum twice its edge count. Enumerate the eight edge subsets and group them by edge count.
Edge count
Number of graphs
Degree sum in each
0
1
0
1
3
2
2
3
4
3
1
6
The table checks the finite cases. A general proof counts vertex-edge incidences: each edge has exactly two endpoints. That argument covers every finite loopless undirected graph, so it supplies more than the enumeration alone.
Understand
A computational proof for a finite domain needs a complete encoding, a coverage argument, a verified decision procedure and inspectable output or certificates. Symmetry reductions can reduce the workload, but they require proof that the property is invariant and every equivalence class is represented. Removing cases because they “look similar” is not a justified reduction.
Loop invariants provide one way to reason about a checker. For a summation loop, after k iterations the accumulator equals the sum of the first k entries. Initialization, preservation and termination establish the result in exact arithmetic. Floating-point addition needs a separate error analysis, so the exact invariant must not be transferred unchanged to computed real sums.
Certified bounds can support numerical conclusions. If a computed value is 0.04 with absolute error at most 0.01, the true value lies in [0.03,0.05] and is positive. A displayed zero with unknown error cannot establish exact vanishing or matrix singularity. Exact rational arithmetic, a verified null vector or interval bounds may provide the appropriate certificate.
Separate four evidence types in a dependency map: proved symbolic steps, external theorems with checked hypotheses, exhaustive finite checks and approximate numerical estimates. The final conclusion cannot silently upgrade an approximate or unproved required step into certainty. A proof sketch is useful when labeled, but its missing arguments remain obligations.
Apply
Choose one finite search relevant to your investigation. Specify the encoding and count the full search space before running it. Provide an independent checker for a returned certificate or a hand-verified small case. Then write the exact domain of the resulting claim and identify what additional theorem would be needed to extend it.
Continue
Mathematical writing makes this evidence structure visible to another reader. A clear report should distinguish the result, assumptions, proof mechanism and computational support without requiring the reader to reconstruct hidden decisions.
Apply · explain · revise
Practice and reasoning
Drafts save locally as you type. Reveal worked solutions when useful; the site remembers that exposure. Automatic matches check the requested answer, while written arguments require review against the rubric.
How many simple labeled graphs on four vertices must an exhaustive edge-subset search inspect?
Integers, fractions and finite decimals are accepted. Expressions such as sqrt(2) are not parsed by this checker.
If a computed value has a certified absolute error at most 1/100 and equals 3/100, what lower bound follows?
Integers, fractions and finite decimals are accepted. Expressions such as sqrt(2) are not parsed by this checker.
What makes a finite exhaustive graph computation a proof for its stated domain?
Structure your argument and preserve revisions
These optional planning fields save locally. Recording your response saves an immutable copy of the argument and these fields. Older records may contain only first/latest responses; missing intermediate revisions are not reconstructed.
Each field allows 2,000 characters. Keep a specific claim, state where it applies, cite the facts you use, and explain what still needs checking. Blank fields are allowed and are not evidence of mastery.
Prove a loop invariant for summing a finite list.
Structure your argument and preserve revisions
These optional planning fields save locally. Recording your response saves an immutable copy of the argument and these fields. Older records may contain only first/latest responses; missing intermediate revisions are not reconstructed.
Each field allows 2,000 characters. Keep a specific claim, state where it applies, cite the facts you use, and explain what still needs checking. Blank fields are allowed and are not evidence of mastery.
Why does a floating-point determinant displayed as zero not prove singularity?
Structure your argument and preserve revisions
These optional planning fields save locally. Recording your response saves an immutable copy of the argument and these fields. Older records may contain only first/latest responses; missing intermediate revisions are not reconstructed.
Each field allows 2,000 characters. Keep a specific claim, state where it applies, cite the facts you use, and explain what still needs checking. Blank fields are allowed and are not evidence of mastery.
Create a proof-and-computation dependency map for one investigation claim.
Structure your argument and preserve revisions
These optional planning fields save locally. Recording your response saves an immutable copy of the argument and these fields. Older records may contain only first/latest responses; missing intermediate revisions are not reconstructed.
Each field allows 2,000 characters. Keep a specific claim, state where it applies, cite the facts you use, and explain what still needs checking. Blank fields are allowed and are not evidence of mastery.
Reflect and continue
Before marking this lesson complete, explain one key idea without the worked solution and identify a condition that matters. Marking complete records participation, not independent mastery.
