AloPex - Math Verification Harness

A general-purpose Math + LaTeX + Linear Algebra + ML verification harness for Cascade/Windsurf agents.

Overview

AloPex provides robust mathematical verification capabilities combining symbolic computation, numerical validation, and formal proof checking. It's designed to help AI agents verify mathematical reasoning, LaTeX expressions, and ML derivations with high confidence.

Technology Stack

Core Python Libraries

• SymPy - Core CAS: parsing, simplification, equivalence, matrix algebra, LaTeX output
• latex2sympy2 - Enhanced LaTeX → SymPy conversion
• math-verify - LaTeX normalization + initial extraction (v0.8.0+)
• PyTorch (torch.autograd) - Automatic differentiation for gradient verification
• NumPy + SciPy - Numerical validation, covariance estimation, finite differences
• mpmath (via SymPy) - High-precision numerical fallback

Formal Verification Integration

• Lean 4 - Formal proof checker for high-stakes mathematical claims
• LeanDojo-v2 - End-to-end framework for AI-assisted theorem proving
• PyPantograph - Machine-to-machine interaction interface for Lean 4
• LeanInteract - Python package for seamless Lean 4 interaction

Installation

# Core dependencies
pip install sympy latex2sympy2 math-verify torch numpy scipy

# With specific antlr4 runtime for math-verify
pip install math-verify[antlr4_13_2]

# Lean 4 integration (optional)
pip install lean-dojo-v2 pypantograph lean-interact

Quick Start

from tools.alopex.math_pipeline import normalize_and_parse, check_equivalence, run_verification_loop

# Parse and normalize LaTeX
latex_expr = r"\frac{d}{dx} \sin(x^2)"
parsed = normalize_and_parse(latex_expr)

# Check equivalence
expr1 = normalize_and_parse(r"\sin(2x)")
expr2 = normalize_and_parse(r"2\sin(x)\cos(x)")
is_equiv = check_equivalence(expr1, expr2)

# Run verification loop with critique
result = run_verification_loop("Prove that derivative of sin(x^2) is 2x*cos(x^2)")

Architecture

graph TB
    subgraph "Math Verification Harness"
        A[LaTeX Input] --> B[math-verify Normalization]
        B --> C[SymPy/latex2sympy2 Parsing]
        C --> D[Symbolic Equivalence Check]
        D --> E{Critical Claim?}
        E -->|No| F[PyTorch/NumPy Validation]
        E -->|Yes| G[Lean 4 Formal Proof]
        F --> H[Verification Report]
        G --> H
    end
    
    subgraph "Cascade Integration"
        I["@math_verifier Skill"] --> A
        H --> J[Iterative Refinement]
        J --> A
    end

Directory Structure

tools/alopex/
├── .windsurf/
│   ├── skills/
│   │   ├── math_verifier/          # Core general math + LaTeX
│   │   │   ├── SKILL.md
│   │   │   ├── harness.py          # Main entrypoint
│   │   │   ├── verifier.py         # SymPy + math-verify + numerical
│   │   │   ├── lean_harness.py     # Lean 4 bridge (optional escalation)
│   │   │   ├── critic.py           # Semantic critique + iteration
│   │   │   ├── prompts/
│   │   │   └── tests/
│   │   ├── linalg_critic/          # Linear algebra specialist
│   │   ├── ml_critic/              # ML gradient verification
│   │   └── leetcode_math/          # LeetCode-style problems
│   ├── AGENTS.md                   # Global math rules
│   ├── math_pipeline.py            # Importable high-level API
│   └── workflows/                  # Optional: verification_workflow.md
└── README.md

Usage Patterns

Basic LaTeX Verification

from tools.alopex.math_pipeline import normalize_and_parse, verify

# Extract and normalize from messy LLM output
messy_output = "The answer is \\boxed{\\frac{\\sqrt{4}}{2}} which equals 1"
normalized = normalize_and_parse(messy_output)

Linear Algebra Verification

from tools.alopex.math_pipeline import verify_linear_properties

# Verify projector properties: A^2 = A, A^T = A
A = sympy.Matrix([[1, 0], [0, 0]])
properties = verify_linear_properties(A, None, M=None)

ML Gradient Verification

import torch
from tools.alopex.math_pipeline import check_gradients

# Verify gradient computations
def loss_fn(x):
    return torch.sum(x**2)

x = torch.randn(3, requires_grad=True)
gradient_correct = check_gradients(loss_fn, x)

Lean 4 Formal Proof (Escalation)

from tools.alopex.math_pipeline import escalate_to_lean

# For critical claims requiring formal proof
claim = "Matrix A is idempotent: A @ A = A"
lean_proof = escalate_to_lean(claim)

Cascade/Windsurf Integration

Skills Usage

Invoke @math_verifier skill for mathematical content:

@math_verifier Prove that the derivative of sin(x^2) is 2x*cos(x^2)

AGENTS.md Rules

The system automatically applies mathematical verification rules:

• LaTeX normalization and parsing
• Symbolic equivalence checking
• Numerical validation
• Lean 4 escalation for critical claims
• Iterative refinement loops

Verification Capabilities

LaTeX Processing

• Robust extraction from messy LLM outputs
• Normalization of \mathrm, boxed answers, malformed operators
• Configurable extraction targets (LatexExtractionConfig, ExprExtractionConfig)

Mathematical Domains

• Calculus: Derivatives, integrals, limits
• Linear Algebra: Matrix operations, eigenvalues, projectors
• Probability: Distributions, expectations, Bayes theorem
• Optimization: Gradients, Hessians, convexity
• ML Theory: Backpropagation, loss functions, regularization

Escalation Policy

• Use SymPy + numerical checks for most cases
• Escalate to Lean 4 for high-confidence critical derivations:
  • Projector geometry properties
  • Procrustes guarantees
  • Flow consistency
  • Exact recovery claims

Performance

• LaTeX Processing: <100ms for typical expressions
• Symbolic Verification: <500ms for standard algebra
• Numerical Validation: <1s for gradient checks
• Lean 4 Proofs: 5-30s depending on complexity

Contributing

See CONTRIBUTING.md for development guidelines.

License

MIT License - see LICENSE file for details.