3> **⚠️ WORK IN PROGRESS - PROTOTYPE ⚠️**
4>
5> **This project is currently a prototype and proof verification is not yet rigorous.**
6>
7> 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.
9A mathematical proof verifier.
11## Overview
13proofery 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.
15Use 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.
17## Features
19- **Full proof verification** - Supports all proof step types including:
20 - `unpack-and`, `cases`, `witness`, `exact`
21 - `calculate` with equational reasoning
22 - `consider`, `forall-apply`, `deconstruct-exists`
23 - `we-have`, `focus-or`, `define`, `assert`, `assert-goal`
24- **Axiom and theorem management** - Collect and verify theorems based on axioms
25- **Clear error messages** - Reports errors with line numbers
26- **Verbose mode** - Optional detailed output during verification
28## Installation
30```bash
31npm install proofery
32```
34Or use directly with npx (no installation required):
36```bash
37npx proofery example.prf
38```
40### Development Installation (from source)
42If you want to contribute or modify the code:
44```bash
45git clone <repository-url>
46cd proofery
47npm install
48npm run build
49```
51## Usage
53### As a Command-Line Tool
55#### Using npx (recommended)
57```bash
58# Basic usage
59npx proofery example.prf
61# With verbose output
62npx proofery --verbose example.prf
63```
65#### Using global installation
67```bash
68# Install globally
69npm install -g proofery
71# Then use directly
72proofery example.prf
73proofery --verbose example.prf
74```
76**Command-line options:**
77- `--verbose`, `-v` - Enable verbose output showing verification progress
78- `--help`, `-h` - Display help message
80### As a Library
82First, install the package:
84```bash
85npm install proofery
86```
88#### In Node.js or TypeScript
90```typescript
91import { parseContent, verifyFile } from 'proofery';
93const prfContent = `
94axiom my_axiom
95 suppose a : Nat
96 conclude eq(a, a)
98theorem reflexivity
99 suppose x : Nat
100 conclude eq(x, x)
101 proof
102 calculate x
103 = x by-lhs my_axiom x
104`;
106try {
107 const blocks = parseContent(prfContent);
108 verifyFile(blocks, false);
109 console.log('✓ Proof verified successfully!');
110} catch (error) {
111 console.error('Verification failed:', error.message);
112}
113```
115#### Parsing from files in Node.js
117```typescript
118import { parseFileSync } from 'proofery/nodeParser';
119import { verifyFile } from 'proofery';
121const blocks = parseFileSync('example.prf');
122verifyFile(blocks, true); // true for verbose output
123```
125#### In the Browser
127You'll need to use a bundler like webpack, vite, or esbuild to use proofery in the browser:
129```javascript
130// Using a bundler (webpack, vite, etc.)
131import { parseContent, verifyFile } from 'proofery';
133function verifyProof() {
134 const content = document.getElementById('proof-input').value;
135 const resultDiv = document.getElementById('result');
137 try {
138 const blocks = parseContent(content);
139 verifyFile(blocks, false);
140 resultDiv.textContent = '✓ Proof verified successfully!';
141 resultDiv.style.color = 'green';
142 } catch (error) {
143 resultDiv.textContent = '✗ Error: ' + error.message;
144 resultDiv.style.color = 'red';
145 }
146}
147```
149For a complete browser example, see `examples/demo.html` in the repository.
151#### Available Exports
153```typescript
154// Main functions
155import { parseContent, verifyFile } from 'proofery';
157// Node.js specific (file parsing)
158import { parseFileSync } from 'proofery/nodeParser';
160// Types
161import { Block, Expression, Context } from 'proofery';
163// Error classes
164import { VerificationError, ParseError } from 'proofery';
165```
167## File Format
169Proof files use the `.prf` extension and consist of:
171- **Axioms** - Statements assumed to be true
172- **Theorems** - Statements that must be proven
174Each theorem includes:
175- `suppose` blocks - Hypotheses and variable declarations
176- `conclude` block - The goal to prove
177- `proof` block - The proof steps
179Example:
181```
182axiom associativity_of_addition
183 suppose a : Nat
184 suppose b : Nat
185 suppose c : Nat
186 conclude eq(add(add(a, b), c), add(a, add(b, c)))
188theorem test1
189 suppose a : Prop
190 suppose b : Prop
191 suppose h1 : a
192 suppose h2 : b
193 conclude and(a, b)
194 proof
195 unpack-and
196 goal a
197 proof
198 exact h1
199 goal b
200 proof
201 exact h2
202```
204For complete language reference, see the original `LANGUAGE_REFERENCE.md`.
206## Development
208Want to contribute? Clone the repository and install dependencies:
210```bash
211git clone <repository-url>
212cd proofery
213npm install
214npm run build
215```
217### Project Structure
219```
220proofery/
221├── src/
222│ ├── index.ts # Library entry point (exports)
223│ ├── cli.ts # CLI entry point
224│ ├── nodeParser.ts # Node.js file parser
225│ ├── parser.ts # .prf content parser
226│ ├── verifier.ts # Main proof verifier
227│ ├── expression.ts # Expression tree representation
228│ ├── block.ts # Block structure
229│ ├── context.ts # Context tracking
230│ ├── simplifier.ts # Expression simplification
231│ ├── calculateVerifier.ts # Calculate step verifier
232│ └── errors.ts # Custom error classes
233├── examples/
234│ └── example.prf # Example proof file
235├── package.json
236├── tsconfig.json
237└── README.md
238```
240### Building
242```bash
243npm run build
244```
246This compiles TypeScript to JavaScript in the `dist/` directory.
248### Testing
250Test the CLI:
252```bash
253npm run build
254npx proofery --verbose examples/example.prf
255```
257Test the library API:
259```bash
260npm run build
261node --input-type=module -e "
262import { parseContent, verifyFile } from './dist/index.js';
263import { readFileSync } from 'fs';
264const content = readFileSync('examples/example.prf', 'utf-8');
265const blocks = parseContent(content);
266verifyFile(blocks, true);
267console.log('\n✓ Library API test passed!');
268"
269```
271## Differences from Python Version
273This TypeScript implementation is a faithful port of the Python version with the following technical differences:
275- Uses TypeScript's type system for enhanced type safety
276- Uses `Map` instead of Python dictionaries for axiom/theorem storage
277- Console output uses Node.js conventions
278- File I/O uses Node.js `fs` module
280The verification logic and proof language remain identical to the Python version.
282## License
284MIT
286## Links
288- [npm package](https://www.npmjs.com/package/proofery)
289- [GitHub repository](https://github.com/magland/proofery)