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