A tool by Alexander S. Petty

nfield

Explore the arithmetic.
See the structure for yourself.

Digit fields, alignment, collision tables, and finite character transforms. The papers develop the mathematics. nfield runs the calculations.

A few places to begin

No installation needed

From the paper to the calculation

Find the command for a mathematical object, inspect one case, then explore its fixed checks. The output distinguishes exact finite arithmetic, numerical calculations, and bounded searches.

Open the paper-to-command guide →

Computational checks show what was tested. They do not replace a universal proof.

Run it on your own machine

Build the public C program with Make, LAPACK, and BLAS. The same command interface is available locally, with shell completion and a JSON/TCP daemon.

git clone https://github.com/alexspetty/nfield.git
cd nfield
make
./nfield field 7
Build requirements and setup →
Use nfield in your work

Research, study, or something commercial?

The software is available under PolyForm Noncommercial 1.0.0. For paid work, products, services, resale, or paid distribution, get in touch about a commercial license. The Lean proofs are separately available under Apache 2.0.

Licensing & commercial inquiries →
Public reference: 9a85687 · Command reference · Lean proofs