proofery

⚠️ WORK IN PROGRESS - PROTOTYPE ⚠️

This project is currently a prototype and proof verification is not yet rigorous.

The verification logic is still under development and should not be relied upon for critical mathematical work. Use at your own risk for experimental purposes only.

A mathematical proof verifier.

Overview

proofery is both a command-line tool and a JavaScript/TypeScript library that verifies mathematical proofs written in the .prf format. It parses proof content, checks the logical validity of theorem proofs, and reports any errors with helpful line numbers.

Use it as a CLI tool to verify .prf files, or import it as a library to integrate proof verification into your web applications or Node.js projects.

Features

• Full proof verification - Supports all proof step types including:
  • unpack-and, cases, witness, exact
  • calculate with equational reasoning
  • consider, forall-apply, deconstruct-exists
  • we-have, focus-or, define, assert, assert-goal
• Axiom and theorem management - Collect and verify theorems based on axioms
• Clear error messages - Reports errors with line numbers
• Verbose mode - Optional detailed output during verification

Installation

npm install proofery

Or use directly with npx (no installation required):

npx proofery example.prf

Development Installation (from source)

If you want to contribute or modify the code:

git clone <repository-url>
cd proofery
npm install
npm run build

Usage

As a Command-Line Tool

Using npx (recommended)

# Basic usage
npx proofery example.prf

# With verbose output
npx proofery --verbose example.prf

Using global installation

# Install globally
npm install -g proofery

# Then use directly
proofery example.prf
proofery --verbose example.prf

Command-line options:

• --verbose, -v - Enable verbose output showing verification progress
• --help, -h - Display help message

As a Library

First, install the package:

npm install proofery

In Node.js or TypeScript

import { parseContent, verifyFile } from 'proofery';

const prfContent = `
axiom my_axiom
    suppose a : Nat
    conclude eq(a, a)

theorem reflexivity
    suppose x : Nat
    conclude eq(x, x)
    proof
        calculate x
            = x by-lhs my_axiom x
`;

try {
    const blocks = parseContent(prfContent);
    verifyFile(blocks, false);
    console.log('✓ Proof verified successfully!');
} catch (error) {
    console.error('Verification failed:', error.message);
}

Parsing from files in Node.js

import { parseFileSync } from 'proofery/nodeParser';
import { verifyFile } from 'proofery';

const blocks = parseFileSync('example.prf');
verifyFile(blocks, true); // true for verbose output

In the Browser

You'll need to use a bundler like webpack, vite, or esbuild to use proofery in the browser:

// Using a bundler (webpack, vite, etc.)
import { parseContent, verifyFile } from 'proofery';

function verifyProof() {
    const content = document.getElementById('proof-input').value;
    const resultDiv = document.getElementById('result');
    
    try {
        const blocks = parseContent(content);
        verifyFile(blocks, false);
        resultDiv.textContent = '✓ Proof verified successfully!';
        resultDiv.style.color = 'green';
    } catch (error) {
        resultDiv.textContent = '✗ Error: ' + error.message;
        resultDiv.style.color = 'red';
    }
}

For a complete browser example, see examples/demo.html in the repository.

Available Exports

// Main functions
import { parseContent, verifyFile } from 'proofery';

// Node.js specific (file parsing)
import { parseFileSync } from 'proofery/nodeParser';

// Types
import { Block, Expression, Context } from 'proofery';

// Error classes
import { VerificationError, ParseError } from 'proofery';

File Format

Proof files use the .prf extension and consist of:

• Axioms - Statements assumed to be true
• Theorems - Statements that must be proven

Each theorem includes:

• suppose blocks - Hypotheses and variable declarations
• conclude block - The goal to prove
• proof block - The proof steps

Example:

axiom associativity_of_addition
    suppose a : Nat
    suppose b : Nat
    suppose c : Nat
    conclude eq(add(add(a, b), c), add(a, add(b, c)))

theorem test1
    suppose a : Prop
    suppose b : Prop
    suppose h1 : a
    suppose h2 : b
    conclude and(a, b)
    proof
        unpack-and
            goal a
                proof
                    exact h1
            goal b
                proof
                    exact h2

For complete language reference, see the original LANGUAGE_REFERENCE.md.

Development

Want to contribute? Clone the repository and install dependencies:

git clone <repository-url>
cd proofery
npm install
npm run build

Project Structure

proofery/
├── src/
│   ├── index.ts              # Library entry point (exports)
│   ├── cli.ts                # CLI entry point
│   ├── nodeParser.ts         # Node.js file parser
│   ├── parser.ts             # .prf content parser
│   ├── verifier.ts           # Main proof verifier
│   ├── expression.ts         # Expression tree representation
│   ├── block.ts              # Block structure
│   ├── context.ts            # Context tracking
│   ├── simplifier.ts         # Expression simplification
│   ├── calculateVerifier.ts  # Calculate step verifier
│   └── errors.ts             # Custom error classes
├── examples/
│   └── example.prf           # Example proof file
├── package.json
├── tsconfig.json
└── README.md

Building

npm run build

This compiles TypeScript to JavaScript in the dist/ directory.

Testing

Test the CLI:

npm run build
npx proofery --verbose examples/example.prf

Test the library API:

npm run build
node --input-type=module -e "
import { parseContent, verifyFile } from './dist/index.js';
import { readFileSync } from 'fs';
const content = readFileSync('examples/example.prf', 'utf-8');
const blocks = parseContent(content);
verifyFile(blocks, true);
console.log('\n✓ Library API test passed!');
"

Differences from Python Version

This TypeScript implementation is a faithful port of the Python version with the following technical differences:

• Uses TypeScript's type system for enhanced type safety
• Uses Map instead of Python dictionaries for axiom/theorem storage
• Console output uses Node.js conventions
• File I/O uses Node.js fs module

The verification logic and proof language remain identical to the Python version.

License

MIT

Links

• npm package
• GitHub repository