Finite Field / Math Lab

Build evidence for correctness, not only fast results.

Math Lab is where we show how we handle mathematical modeling, theorem proving, formal verification, reproducibility, and trusted implementation without overstating the evidence.

View research areas Open the NPA page

Public projects: NPA / STD / MATHLIB
Core language: Rust
NPA snapshot: v0.1.1

Public readback: 2026-06-28. NPA public status and method-review wording were checked; final publication readback remains for M10-T14.

Proof audit / conceptual view Read only

01 canonical bytes / format OK

02 certificate_hash OK

03 dependent proof checking OK

04 source-free verdict OK

Trust boundary visible

This page does not claim that NPA is a practical replacement for Lean or Rocq, and the browser simulation does not execute NPA.

Lab principle

Publish not only results, but also the boundary of checking.

A conclusion such as “it worked,” “it was fast,” or “it was proven” is not enough. We show inputs, assumptions, trusted parts, independently checkable artifacts, and unresolved issues separately.

01 / Boundary

Keep the trusted base small

Do not place complex generators or AI at the center of trust. Make the small checking side explicit.

02 / Evidence

Make evidence an artifact

Leave certificates, hashes, assumption lists, benchmark conditions, and logs in a form others can inspect.

03 / Reproduce

Design for reproducibility

Pin toolchains, input data, execution commands, and criteria so the result can be checked again.

04 / Honesty

Do not overstate research status

Show practical methods, experiments, and research separately. Put limitations beside results.

METHOD REVIEW

A service-method category that still requires scope, responsibility, client evidence, and approval before being described as project-ready.

EXPERIMENTAL

A working implementation exists, but scale, compatibility, performance, or specification changes remain possible. Version and reproduction steps are required.

RESEARCH

Design, evaluation, proof, or implementation is ongoing. This does not imply commercial availability or completion.

Research portfolio

View research by maturity and artifacts.

Each card shows the maturity, artifacts, current state, and next validation. Search and filters use only browser-side state.

8 shown

EXPERIMENTAL OPEN SOURCE

Nano Proof Auditor

Certificate-first proof toolchain

A research toolchain that places canonical proof certificates and a small checking base at the center of dependent proof review.

Artifacts: source / specification / CI templates
Current: v0.1.1 public snapshot
Next validation: external theorem packages and independent checking

Open NPA detail

EXPERIMENTAL OPEN SOURCE

NPA Standard Library

Logic / Nat / List / Algebra

A standard theorem package repository for reusable NPA foundations.

Artifacts: source / proof packages
Current: public split repository
Next validation: package scope and compatibility

GitHub

RESEARCH OPEN SOURCE

NPA Math Library

Formal mathematics library

A library direction for storing mathematical theorems as independently checkable proof packages.

Artifacts: source / proof packages
Current: public repository under development
Next validation: library structure and dependency audit

GitHub

METHOD REVIEW METHOD

Constrained planning models

Scheduling / Routing / Assignment

A method for separating hard constraints and evaluation metrics in shifts, visits, routing, production, and assignment work.

Artifacts: model / prototype / explanation report
Current: service method; public claim limited to method review
Next validation: client evidence and scope approval

View prototype

RESEARCH MEASUREMENT

Reproducible solver evaluation

Benchmark and evidence

A program for fixing instance sets, hardware, time limits, random seeds, and raw logs before making performance claims.

Artifacts: benchmark registry / raw logs / report
Current: research-program design
Next validation: first public benchmark corpus

View method

RESEARCH FORMAL METHODS

Verification for critical business logic

Invariants for business systems

Research on separating fees, permissions, inventory, and state transitions into specifications and invariants.

Artifacts: specification / invariants / test or proof report
Current: scope study
Next validation: select one bounded production-like case

View security design

EXPERIMENTAL ENGINEERING

Small trusted components in Rust

Small trusted components

Implementation work that keeps trust-critical pieces such as checkers and hashes small enough to inspect.

Artifacts: NPA kernel / certificate crate / reference checker
Current: public implementation in NPA
Next validation: independent checker compatibility

View source

RESEARCH AI × PROOF

AI assistance and independent checking

Generate freely, verify strictly

A research direction that places AI on candidate generation while the final evidence is independently checked.

Artifacts: candidate generator / certificate / checker report
Current: research direction consistent with NPA trust model
Next validation: measured authoring workflow

View trust boundary

No matching research area was found.

Try another keyword or return the maturity filter to all.

Nano Proof Auditor

Separate proof generation from what we trust.

NPA is a certificate-first proof toolchain for dependent proofs. Front ends, tactics, theorem search, plugins, AI, source files, and CI status can help create candidates, but they are not the trusted proof evidence.

EXPERIMENTALOPEN SOURCEAPACHE-2.0

Current snapshot

v0.1.1

Public information checked on 2026-06-21.

Primary core

Rust

Rust verifier and kernel are part of the checking side.

Audit artifact

.npcert

Canonical certificate bytes are the object to inspect.

Recheck point

manual review

Repository state and package visibility must be reviewed before publication.

Trust boundary explorer

Click through what is trusted and what is not.

Click each node to inspect what it does, what it produces, and which check is still required.

UNTRUSTED

CHECKED

Important boundary

NPA is not currently a practical replacement for Lean or Rocq. This page explains certificate-centered research design and does not guarantee bug-free commercial systems or automatic theorem solving.

Certificate check / explanatory simulation

Experience the flow of certificate checking.

The browser interaction explains the inspection flow. It does not run NPA, Rust, WASM, or real proof certificates.

CLI example

npa package verify-certs --root . --checker reference --json

NPA / audit trace READY

01 Read the certificatecanonical bytes / format WAIT
02 Check the certificate hashcertificate_hash WAIT
03 Check with the kerneldependent proof checking WAIT
04 Recheck with the reference checkersource-free verdict WAIT
05 Compare the axiom reportaxiom report hash WAIT

Verdict

The explanation has not run yet.

Run the explanation to visualize the steps in order.

Proof ecosystem

Clarify roles instead of ranking tools.

Lean and Rocq are mature proof-assistant ecosystems. NPA is shown here as a certificate-centered research and implementation project, not as a replacement ranking.

Item	Lean	Rocq	NPA
Position	Open-source programming language and proof assistant.	Interactive theorem prover with a long research history.	Research and implementation repository for certificate-first checking.
Typical use	Mathematics, software verification, and programming.	Mathematics, specifications, program verification, and extraction.	Research into proof certificates and independent checking.
Emphasis	Extensibility, libraries, and interactive proving.	Expressiveness, mature methods, and libraries.	Small trusted base and canonical certificates.
How this page treats it	Reference for learning, comparison, and interoperability.	Reference for learning, comparison, and formalization methods.	Finite Field research project.
Boundary	Specialist knowledge is still required.	Specialist knowledge is still required.	Not intended as a practical replacement for Lean or Rocq at this time.

Lean official site Rocq Prover official site NPA GitHub

Research method

Turn “it worked” into a repeatable checking procedure.

A result becomes stronger when someone can rerun, inspect, and reject it under the same conditions.

Question

Define what should be checked: performance, correctness, compatibility, or scope.

Assumptions

Write assumptions, exclusions, axioms, data gaps, and bias before evaluation.

Artifact

Keep source, certificates, inputs, execution logs, and hashes.

Independent check

Check results through a path different from the generation side.

Benchmark

Fix hardware, versions, time limits, instance sets, and random seeds.

Limits

Publish failures, unsupported cases, performance boundaries, and next validation.

Reproducibility builder

Check what a research publication still lacks.

The checklist is processed only in the browser. It is not a certification score.

Readiness

Research question and success conditionWhat counts as success or failure. Pinned tools and dependenciesVersions, lock files, hardware, and environment. Input data or generation processAnonymization, license, source, and hash. Re-run command sequenceFrom initialization through result generation. Checkable artifacts and raw logsCertificates, reports, logs, and hashes. Limits, failures, and open questionsUnsupported cases and unresolved issues.

Next action

Define the research question and success condition first.

Before deciding artifact formats, fix what will be compared or checked.

Public artifacts

Track public artifacts from one entrance.

The page avoids runtime GitHub API calls. Repository state is a reviewed snapshot that must be checked before publication.

4 artifacts

finitefield-org

npa

certificate-first proof toolchain

Rust / OCamlApache-2.0Experimental

Open

finitefield-org

npa-std

standard theorem package

ProofsPackageExperimental

Open

finitefield-org

npa-mathlib

formal mathematics library

MathematicsProofsResearch

Open

GitHub

finitefield-org

public repository index

OrganizationOpen source

Open

No public artifact matches the search.

Publication policy

Public repositories, research notes, and benchmarks should carry the checked date, maturity, reproduction steps, and known limitations. Stars and commit counts are not shown as research-quality signals.

From Lab to operations

Bring research discipline into business system design.

Not every client system needs theorem proving. The useful transfer is deciding what must be trusted, compared, checked, corrected, and approved by people.

Lab practice

Trust boundaries

Separate generation, calculation, and final checking instead of trusting every layer equally.

Evidence

Keep inputs, outputs, certificates, hashes, and logs as reviewable artifacts.

Reproducibility

Pin data, versions, commands, and evaluation criteria before comparing results.

Limits

Publish constraints, failed cases, and unresolved points with the same weight as results.

Client system

Authority and responsibility

Define who inputs, who reviews, who overrides, and who confirms the result.

Decision reasons

Show constraints, evaluation scores, rejected candidates, and unresolved points.

Auditability

Preserve condition changes, calculation runs, and final approval history.

Human judgment

Make automated output correctable, rejectable, and explainable to operators.

01 Shift and staffing

Show rule violations and preference satisfaction separately.

02 Vehicle routing

Keep route reasons, capacity, time windows, and exceptions visible.

03 Production scheduling

Explain unscheduled work, bottlenecks, and setup trade-offs.

04 Assignment matching

Display candidate reasons and alternatives before approval.

Research notes

Keep update history and evidence readable.

Not every card is a published article. Preparing notes remain unlabeled as published work until they receive dates, sources, and reproduction steps.

NPA / Current2026.06.21

Why place certificates at the center

Why final evidence should be a standardized certificate checked by a small independent path.

View public repository

Design note / plannedPreparing

Making optimization results explainable

A design note about exposing objectives, hard constraints, soft preferences, and unresolved assignments in UI.

View related demos

Benchmark / plannedPreparing

Conditions for fair solver comparison

A planned note about instance sets, time limits, optimality gaps, random seeds, and hardware.

View publication criteria

“Preparing” items are not published articles. After publication, each note receives a date, source, author, reproduction path, and known limitations.

FAQ

Research, proof tools, and business use boundaries.

These points are made explicit before research pages are mistaken for production guarantees.

Read about the company

01 Is Math Lab a contract development service?

No. It is a place to publish research attitude and artifacts. In client discussions, we separate applicable methods, methods that need more validation, and research-stage topics.

02 Can NPA replace Lean or Rocq?

No. Current NPA is not a practical replacement for Lean or Rocq. It is a research and implementation project around certificates, independent checking, and a small trusted base.

03 Do you trust AI-generated proofs as they are?

No. AI, search, and tactics help generate candidates. We focus on whether the final certificate is accepted by a checker independent of those generation paths.

04 Does formal verification remove all bugs?

No. Formal methods check specific properties against an explicit specification. Wrong specifications, out-of-scope code, operations, and external services still need separate review.

05 Does this relate to business system work?

Yes. We usually apply the discipline gradually: constraints, result reasons, calculation history, permission boundaries, and checks for important business logic.

Discuss a problem

You can discuss the work to solve, not only the research topic.

Start from the current spreadsheet, rules, and places where decisions are corrected by people. We can sort out whether mathematical modeling, rule automation, or a prototype should come first.

Check the business issue View prototype

Source snapshot / 2026-06-21

NPA claims are based on the finitefield-org/npa repository snapshot. Lean and Rocq positioning is based on their official sites. Repository state, latest tags, and method-review wording were checked on 2026-06-28; final publication readback remains.