Binary, the engine, the vision. His binary arithmetic is the language of every computer; his Stepped Reckoner did all four operations; and "Calculemus!" named the goal — mechanise reasoning — that all of computing pursues.
A program, not a building. The universal characteristic and the calculus of reasoning were never completed; his logical algebra sat unpublished for two centuries, so Boole re-found it independently.
The dream has a ceiling. Gödel (1931) and Turing (1936) proved no method can decide every truth by calculation. Reasoning can be mechanised — but not completely. Half the dream came true.
Leibniz worked out base-two arithmetic and was moved by it almost to mysticism: from 0 (nothing) and 1 (God), all numbers. Toggle the bits below and watch any number appear as a pattern of ons and offs — the exact representation a memory cell holds, and the only thing a logic gate can read. It would take 250 years for the machines to catch up to the notation.
128 64 32 16 8 4 2 1 · the number is the sum of the lit places — and that is all a register ever is.Here is the dream made concrete, and it's Leibniz's own idea (1679): give each basic attribute a prime number, and let a concept be the product of its attributes' primes. Then a syllogism becomes a division. "All men are animals" is valid exactly when the number for animal divides the number for man — because to be a man is to already contain being an animal. Build the concept "man" from its attributes and watch every inference settle by pure arithmetic.
"The only way to rectify our reasonings is to make them as tangible as those of the mathematicians, so that we can find our error at a glance… and say to each other: Let us calculate." — Leibniz
Leibniz was the last universal genius — co-inventor of the calculus (whose notation dx, ∫ we still use, won despite the bitter priority war with Newton), a working diplomat, jurist, historian and engineer, builder of the four-operation Stepped Reckoner, and the philosopher of monads and "the best of all possible worlds." He read Llull, and reached past him toward a machine that could reason.
Gate kept on. The vision was breathtaking and the execution thin. The characteristica universalis and the calculus ratiocinator were a lifelong program he never finished — sketches and fragments, not a working system; his prime-number logic handled "all/some" only awkwardly and stalled on negation. His logical algebra stayed unpublished until ~1900, so it had almost no influence and Boole rediscovered the territory on his own. And the deepest twist: the full dream — a calculation that settles every dispute — was proven impossible. Gödel showed any rich formal system has true statements it cannot prove; Turing showed no machine can decide all of them. Reasoning can be mechanised — that half came true and runs on your desk — but not completely. Leibniz pointed at the future and got the direction exactly right and the limit exactly wrong.