<_RESEARCH/PROJECTS

Heyting Base Contracts

DEPLOYED0 SORRY5 MENTAT CERTSLean 4 + Solidity

>_VERIFICATION.SEAL

Formal Verification Certificate

All invariants formally verified in Lean 4. Contracts deployed on Base Sepolia.

0 SORRY

Heyting Base Contracts • Lean 4 + Mathlib • Apoth3osis Labs

❓

The Central Question

Can mathematical proofs be published as on-chain attestations? This project deploys three smart contracts on Coinbase’s Base: a verification oracle that stores proof verification results immutably, NFT audit certificates (ERC-721) representing verified theorems, and ZK credentials enabling privacy-preserving proof of verification status. The contract invariants are themselves formally verified in Lean 4.

Key Verified Results

oracle_consistency

No conflicting attestations for same proof hash

Oracle.lean

certificate_unique

One NFT per verified proof (no duplicates)

Certificate.lean

credential_sound

ZK proofs verify only for valid attestations

Credential.lean

Resources

GHGitHub Repository IDXAll Research Projects

⊢⊣⊢⊣

>_MENTAT.JOIN

“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune

A janitor who proves a theorem outranks a tenured professor who publishes noise.

Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.

ONTOLOGICAL ENGINEER8 designations

IDEA

A valid, original framing or conjecture

THEORY

Formal argument with paper-level rigor

APPLICATION

Connecting theory to observable outcomes

CODE

Working software the project depends on

EXPERIMENT

Reproducible research with methodology and data

PROOF

Machine-verified claim checked by a proof assistant

KERNEL

Foundational, load-bearing implementation

BRIDGE

Connecting subsystems or knowledge domains end-to-end

NOETIC ENGINEER8 designations

VISIONARY

Strategic direction & roadmaps

NARRATOR

Writing, documentation & papers

DESIGNER

Visual, UX & information design

EDUCATOR

Teaching, tutorials & workshops

CULTIVATOR

Community, outreach & events

DIPLOMAT

Partnerships, governance & policy

INTERPRETER

Translation, media & accessibility

SENTINEL

Ethics, review & quality assurance

Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.

APPLY TO MENTAT EXPLORE PROJECTSMESH-ENCRYPTED NETWORK FOR TRUSTED AUTONOMOUS TRANSACTIONS

>_MENTAT.CERTIFICATES

Contribution Certificates

Immutable contribution records per MENTAT-CA-001. Each certificate is cryptographically anchored with IPFS CIDs.

MENTAT-CA-001|MCR-HBC-001

2026-01-20

MENTAT Contribution Record

IDEA

Conceptual Contribution

CONTRIBUTION LEVEL: IDEA

Ontological Engineer

On-Chain Verification Oracle for Formal Mathematics

Contributor

Apoth3osis Labs

R&D Division

Core insight: Lean 4 proof verification results can be published as on-chain attestations, creating immutable audit trails. NFT certificates represent verified proofs, and ZK credentials enable privacy-preserving proof of verification status.

MENTAT · Mesh-Encrypted Network for Trusted Autonomous TransactionsImmutable · Content-Addressed · Tamper-Proof

MENTAT-CA-001|MCR-HBC-002

2026-01-20

MENTAT Contribution Record

THEORY

Mathematical Foundation

CONTRIBUTION LEVEL: THEORY

Ontological Engineer

Three-Layer Contract Architecture

Contributor

Apoth3osis Labs

R&D Division

Complete framework: (1) Verification Oracle — accepts proof hashes and verification status, stores results immutably, (2) NFT Audit Certificates — ERC-721 tokens representing verified proofs with metadata pointing to IPFS artifacts, (3) ZK Credentials — zero-knowledge proofs of verification status without revealing the proof content.

Builds Upon

MCR-HBC-001

MENTAT · Mesh-Encrypted Network for Trusted Autonomous TransactionsImmutable · Content-Addressed · Tamper-Proof

MENTAT-CA-001|MCR-HBC-003

2026-01-20

MENTAT Contribution Record

PROOF

Formally Verified

CONTRIBUTION LEVEL: PROOF

Ontological Engineer

Lean 4 + Solidity Formalization

Contributor

Apoth3osis Labs

R&D Division

Machine-checked Lean 4 formalization of the contract invariants: oracle consistency (no conflicting attestations), certificate uniqueness (one NFT per proof), and credential soundness (ZK proofs verify only for valid attestations). Solidity contracts deployed and tested on Base Sepolia.

Builds Upon

MCR-HBC-001MCR-HBC-002

MENTAT · Mesh-Encrypted Network for Trusted Autonomous TransactionsImmutable · Content-Addressed · Tamper-Proof

MENTAT-CA-001|MCR-HBC-004

2026-01-25

MENTAT Contribution Record

KERNEL

Computationally Verified

CONTRIBUTION LEVEL: KERNEL

Ontological Engineer