Math Verify

Verification Patterns

Claim: (x+1)^2 = x^2 + 2x + 1

claimed = (x+1)2 expanded = expand(claimed) expected = x2 + 2*x + 1

print(f"Claimed expansion: {expanded}") print(f"Expected: {expected}") print(f"Match: {simplify(expanded - expected) == 0}")

</pattern>

<pattern name="Check Limit Arguments">
```python
from sympy import *
x, n = symbols('x n')

# Verify limit claim: lim_{x->0} sin(x)/x = 1
result = limit(sin(x)/x, x, 0)
print(f"Computed limit: {result}")
print(f"Claimed limit matches: {result == 1}")

# Check L'Hopital applicability
numerator_at_0 = sin(x).subs(x, 0)
denominator_at_0 = x.subs(x, 0)
print(f"0/0 form: {numerator_at_0 == 0 and denominator_at_0 == 0}")

x = symbols('x', real=True)

Claim: x^2 - x >= 0 for all x not in (0,1)

inequality = x**2 - x >= 0 solution = solve_univariate_inequality(inequality, x, relational=False) print(f"x^2 - x >= 0 when: {solution}")

Should give: (-oo, 0] U [1, oo)

</pattern>

<pattern name="Test Edge Cases">
```python
import numpy as np

def test_claim(f, test_points, expected_behavior):
    """Test a claimed property at specific points."""
    results = []
    for x in test_points:
        try:
            y = f(x)
            results.append((x, y, expected_behavior(x, y)))
        except Exception as e:
            results.append((x, "ERROR", str(e)))
    return results

# Example: test claim that f(x) > 0 for all x > 0
f = lambda x: x**2 - x + 0.25  # (x - 0.5)^2
test_points = [0.001, 0.5, 1, 10, 1e-10]
for x in test_points:
    print(f"f({x}) = {f(x)}, > 0: {f(x) > 0}")

Example: Mean Value Theorem requires:

1. f continuous on [a,b]

2. f differentiable on (a,b)

from sympy import * x = symbols('x')

Check if f = |x| satisfies MVT hypotheses on [-1, 1]

f = Abs(x) print(f"f = {f}") print(f"Continuous on [-1,1]? Yes (absolute value is continuous)") print(f"Differentiable at 0? No (corner point)") print("CONCLUSION: MVT does NOT apply here!")

</pattern>

<pattern name="Pathological Counterexamples">
```python
import numpy as np

# Weierstrass function: continuous but NOWHERE differentiable
def weierstrass(x, a=0.5, b=7, n_terms=50):
    return sum(a**n * np.cos(b**n * np.pi * x) for n in range(n_terms))

# Test: if proof assumes "continuous => differentiable somewhere"
x_test = np.linspace(0, 1, 1000)
y_test = [weierstrass(x) for x in x_test]
print("Weierstrass function is continuous everywhere")
print("But differentiable NOWHERE - counterexample to naive assumption")

# Indicator function of rationals: discontinuous everywhere
# (useful for checking integrability claims)

Common Proof Errors Checklist

Domain-Specific Checks

Analysis Proofs

• epsilon-delta arguments have correct quantifier order
• Limit computations verified with SymPy
• Continuity checked at boundary points
• Tested with Weierstrass, Dirichlet functions

Algebra Proofs

• Group/ring axioms actually satisfied
• Homomorphism properties verified
• Tested with small examples (Z_n, S_3, D_4)

Induction Proofs

• Base case computed explicitly (not just "obviously true")
• Inductive hypothesis clearly stated
• Inductive step actually uses the hypothesis

Output Format

## Claim Being Verified
[Exact statement of theorem/claim]

## Proof Structure
- Type: [direct/contradiction/induction/...]
- Key techniques: [...]

## Step-by-Step Verification

### Step 1: [description]
- **Claim**: [what this step asserts]
- **Justification**: [author's reasoning]
- **Verification**:
```python
# Computational check

• Status: VERIFIED / UNVERIFIED / INVALID
• Issues: [if any]

Step 2: ...

[continue for each step]

Edge Cases Tested

Counterexample Search

• Tried: [list attempts]
• Result: None found / FOUND: [describe]

Issues Summary

1. [Issue 1]
2. [Issue 2] ...

Verdict

VALID / VALID WITH MINOR ISSUES / INCOMPLETE / INVALID

Confidence: HIGH / MEDIUM / LOW Reason: [why this confidence level]