MLambda.AI

MLambda.AI · samples you can read, run and prove

Artificial intelligence, written so you can check it.

Logic, agents, machine learning, reinforcement learning and the mathematics under them, each one real Hilbert source that the build compiles and checks, with a test asserting what it does. Nothing here is pseudocode, and a proof that stops checking stops the build.

Start with Hilbert → Why it matters Pick your level Source on GitHub

3levels, novice to advanced

6subjects at every level

94theorems the kernel checks

404tests asserting behaviour

Animals.hs

theory Animals (Thing)
{
  def kind_of(narrow: Thing, wide: Thing)
  def known(who: Thing, kind: Thing)

  -- what you are told becomes what is so
  law directly = ∀ x k, known(x, k) ⇒ is_a(x, k)

  -- and classification climbs
  law climbing = ∀ x k w, is_a(x, k) ∧ kind_of(k, w) ⇒ is_a(x, w)

  query kinds(of: Thing, kind?: Thing) :- is_a(of, kind)
}

› What is fluffy?  cat, animal
  'animal' is in that list and nobody put it there.
› Proved  a_cat_is_an_animal
› Proved  classification_climbs_twice

How to use this site

Four steps. The first is short and every sample assumes it; the last is what the other three were for.

Learn HilbertSix short pages: the four dialects, the build, reading a proof. Level 1 · NoviceFacts, rules, and a machine working out what nobody wrote down. Levels 2 and 3What the notation buys you, then proving things about the systems. The capstoneOne real house, three agents, one verdict.

Why it matters

Four short essays, no code required: what it takes to put a thought into a machine, and why it is not a prompt.

Minds

Putting a thought into a machine

Why belief, knowledge and intention defeat tables and text, and how possible worlds make them tractable.

Read →

Logic

The modal systems, explained

K, T, D, S4, S5, KD45: six choices about what an attitude may do, and how to pick them for a real problem.

Read →

Accountability

When a chatbot makes a promise

An airline paid for its chatbot's answer. What the answer meant, and the problems semantics solves.

Read →

Neuro-symbolic

A network that proposes, a logic that checks

Why AlphaGeometry and AlphaProof pair a model with a verifier, and what chain-of-thought cannot give you.

Read →

Three levels

Every subject appears at each of them. A page is L1 because it is on the L1 shelf, so start where you are and climb.

Level 1 · Novice

Your first reasoning machine

You have never written a rule for a computer to reason with. You will state facts and rules separately and watch consequences appear.

• Animals, Families, Chains
• A thermostat that intends
• A line found from its points
• A bandit that learns
• Traffic lights and duties
• A law that folds a formula away

Start L1 →

Level 2 · Practitioner

What the notation buys you

You can read a theory and want to know why it is written that way: modal frames, certificates, agents that commit and give up.

• Worlds and Counting
• Collector and Cleaner
• Perceptron and Classifier
• Q-table and Sarsa
• Knowing vs believing
• A derivative, and one that cannot be taken

Start L2 →

Level 3 · Advanced

Proving things about the systems

You want guarantees, not only programs: the theory beneath every agent, the law that is missing on purpose, the algebra learners stand on.

• Sorts, and the missing law
• Agency: belief, desire, intention
• Nearest, and what is not claimed
• Identities, proved by the kernel
• Deadlines, and who knew
• Three grades of certainty

Start L3 →

Every subject, at every level

Read across a row to follow one subject from its first idea to its proofs, or down a column to take a whole level at once.

	L1 · Novice	L2 · Practitioner	L3 · Advanced
Logictheorem proving	Animals, Families, Chainsa rule works out what nobody wrote down	Worlds and Countingmodal frames, arithmetic by certificate	Sortsand the law that is missing
Mindstime, duty, knowledge	Traffic and Dutyalways, eventually, and what ought to be	Knowledge and Mindknowing is not believing	Deadlinesand what these logics cannot say
Agentsbelief, desire, intention	Thermostata goal that never changes, intentions that do	Collector and Cleanercommitment, attention, giving up	Agencythe theory underneath every agent
Machine learningmodels in .hb	Linea model is a formula you can read	Perceptron and Classifierweights, and an instructive failure	Nearestand what this project does not claim
Reinforcement learninglearning from reward	Banditexplore or exploit	Q-table and Sarsatwo learners, one line of source apart	Identitiesthe algebra, proved
Mathematicslaws in .hb, proved in .hp	Algebrathe answer arrives with its reason	Calculus and Solvea derivative taken before you ran anything	Linear and proofthree grades of certainty

One language, four dialects

One compiler and one token set. Each file extension says a different kind of thing. Read the tour →

.hs

A theory: relations, Horn laws, queries. It becomes an engine you assert facts into and ask questions of.

.hp

Theorems over a theory, discharged by proof … qed and checked by a small kernel.

.ha

An agent: beliefs, desires, intentions, commitment, attention and plans.

.hb

Mathematics: formulas, models and processes over tensors and reals, lowered to code.

The capstone · read after L3

One house. Three agents. One verdict.

A buyer looks at a real house from 2 930 Ames sales. A valuation model, a condition model and a credit model each form a belief and an intention, and an adjudicator decides — with a veto, and a reserve that may refuse to exist.

Open the capstone →

ValuationAgent   +0.07 spreads over     → Buy
ConditionAgent   repair $17,523         → Negotiate
CreditAgent      default chance 30.40%  → Walk

Adjudicator      Walk. One agent seeing ruin
                 outranks two seeing a bargain.

Running the samples yourself. The Hilbert compilers are not on NuGet yet, so the repository builds against a sibling checkout of MLambda.Genesis. Clone both side by side, then dotnet build MLambda.AI.slnx and dotnet test MLambda.AI.slnx. Every sample page ends with the command that runs it.