Documentation

How it all works. The math, the code, the chain.

What is Gödel?

Gödel is an automated theorem proving engine. It uses Claude (Fable 5) to generate formal proofs, verifies them with the Lean 4 proof assistant, and records every verified result on Robinhood Chain.

Over time this builds a public, growing log of machine-discovered math that anyone can check.

Every proof can be checked by anyone. Download the Lean 4 code, run it, hash it, compare to the chain.

Why it matters

Most AI research is a black box. You read a paper, trust the authors, hope it replicates. This is different:

The namesake

Kurt Gödel (1906-1978) proved that in any consistent mathematical system, there are true statements that can never be proved within that system. His incompleteness theorems changed mathematics forever.

This project carries his name because we're working at the same edge: what can machines actually prove? Some theorems will be out of reach. That's the point. Push the boundary and see what falls.

The pipeline

Every proof goes through four stages:

  1. Conjecture selection // a mathematical statement is pulled from the research queue
  2. Proof generation // Claude (Fable 5) writes a formal proof candidate in Lean 4
  3. Verification // Lean 4 + Mathlib compiles the proof. If it builds, it's correct.
  4. Anchoring // the proof code is SHA-256 hashed and registered on GodelRegistry
Conjecture → Claude generates Lean 4 proof → lake build → ✓ or ✗
                                                             ↓
                                                 SHA-256 hash → on-chain

Lean 4

Lean 4 is a programming language and theorem prover from Microsoft Research. Mathematicians use it to formalize proofs.

Key properties:

Lean doesn't care who wrote the proof. Human, AI, random noise. If it type-checks, it's valid math.

Mathlib

Mathlib is the community math library for Lean 4. Hundreds of thousands of formalized definitions, lemmas, and theorems:

Gödel builds on top of Mathlib. Proofs can reference any existing theorem in the library, standing on centuries of formalized math.

Verification

When we say a proof is "verified," we mean:

$ cd godel/lean-project
$ cat Godel/Proof.lean
import Mathlib.Tactic

theorem even_sum (n : ℕ) : Even (n + n) := ⟨n, rfl⟩

$ lake build Godel
✓ Built Godel.Proof
Build completed successfully.

If lake build succeeds, Lean's kernel has verified every step. Not by peer review, not by reputation. By math.

Robinhood Chain

All proofs are anchored on Robinhood Chain (chain ID 4663), an EVM-compatible blockchain.

GodelRegistry

GodelRegistry stores every verified proof on-chain. Each entry looks like this:

struct Proof {
    string theoremId;
    string name;
    string statement;
    bytes32 proofHash;
    uint256 timestamp;
    string difficulty;
}

Public functions:

Proof hashing

The proof hash is computed as:

SHA-256( lean_4_proof_source_code )

Same code, same hash, every time. Change one character and the hash is completely different. What's on-chain is a permanent commitment to a specific proof.

Verify a proof yourself

Complete verification in three steps:

# 1. Get the proof hash from the chain
cast call $REGISTRY "getProof(uint256)" 0 --rpc-url https://rpc.mainnet.chain.robinhood.com

# 2. Get the Lean 4 source code (from our repo or site)
cat proof_even_sum.lean

# 3. Hash it and compare
echo -n "$(cat proof_even_sum.lean)" | sha256sum
# should match the on-chain proofHash

If the hashes match and lake build succeeds on the Lean code, the proof is independently verified end-to-end.

Research approach

Not trying to crack the Riemann Hypothesis on day one. The approach is incremental:

  1. Start simple // prove known theorems to validate the pipeline
  2. Scale difficulty // harder problems as techniques improve
  3. Generate conjectures // use AI to propose new statements, then try to prove them
  4. Publish findings // novel results go to arXiv with full Lean 4 formalization

Conjecture categories