Block I · Foundations of Knowledge & Reasoning · Day 003 / 180
Logic & Valid Inference
Three ways to move from what you know to what you don't — and only one of them is safe.
A stranger walks into a London consulting room. Within seconds Sherlock Holmes announces, to Watson's astonishment, that the man is a retired army doctor, recently invalided home from Afghanistan. The skin is tanned but the wrists are pale — a sunburn caught abroad, not at the seaside. He holds his arm stiffly, war-wounded. The face is haggard with hardship and fever. Holmes calls this deduction, and the word has clung to him for over a century. He is wrong about the word. What Holmes performs — and what made him immortal — is not deduction at all. It is a humbler, riskier, far more creative thing.
That mislabeling is the perfect way in, because the whole of today turns on a distinction almost everyone blurs: there is more than one way to reason, and they do not come with the same guarantees. Some inferences are airtight — if you grant the premises, the conclusion cannot escape. Others are fertile but fallible — they reach past the evidence and can be overturned by tomorrow's surprise. Mistaking one for the other is the root of a startling fraction of human error. So let's draw the lines carefully.
◆ Where we are
Two days in, we have circled reasoning from the outside. On Day 1 we asked what turns a true belief into knowledge — and hit the Agrippan trilemma, the worry that every justification either regresses forever, loops in a circle, or stops somewhere arbitrary. On Day 2, Hume's problem of induction showed that no pile of observations can ever prove a universal law, which is why Popper told us to falsify rather than verify. Today we open the engine itself. Those two earlier puzzles were really about the limits of two specific inference modes; now we name all three, watch logic become mathematics, and follow it to the strangest frontier in the course — machines that check proofs with zero tolerance for error. The thread that lights up brightest today is computation.
The model
Three engines, three guarantees
If you remember one thing from today, make it this trichotomy. Reasoning is not one activity but three, and they are sorted by how much they promise.
Deduction is the truth-preserving engine. The conclusion is already folded inside the premises; valid deduction merely unfolds it. Grant that all men are mortal and that Socrates is a man, and you cannot avoid the conclusion that Socrates is mortal — to deny it is to contradict yourself. The price of this safety is that deduction is non-ampliative: it never tells you anything genuinely new about the world. It rearranges what you already have. Mathematics is the deductive art carried to its limit, which is exactly why mathematicians can be so certain and why their certainty never, by itself, settles a question about this universe.
Induction is the generalizing engine. You have seen the sun rise ten thousand times; you infer it will rise tomorrow. Every swan anyone had ever logged was white, so — until 1697 — "all swans are white" looked secure. Induction is ampliative: it adds content, reaching beyond the cases in hand. And for precisely that reason it is not truth-preserving. This is Hume's bomb from Day 2, still ticking: no finite run of observations can logically guarantee the next one. Induction is how empirical knowledge actually grows, and it comes with no warranty.
Abduction is the explaining engine — and the one most people were never taught to name. You meet a surprising fact, and you cast around for a hypothesis that, if true, would make the surprise dissolve. The American polymath Charles Sanders Peirce (1839–1914) singled it out as the only genuinely creative mode, the one that generates new ideas rather than just testing or unpacking them. "Every plank of [science's] advance," he wrote, "is first laid by retroduction alone." Deduction and induction work over hypotheses you already have; abduction is where the hypotheses come from in the first place.
Now back to Holmes. The tan, the stiff arm, the haggard face — these are surprising facts, and Holmes leaps to the explanation that best accounts for all of them at once: a war-wounded military doctor home from a hot campaign. But notice the leap is not guaranteed. The man could be an actor who summers in Morocco and sprained his shoulder playing tennis. Holmes's conclusion is the best explanation, not the only one — which is the signature of abduction, not deduction. Conan Doyle gave his detective the wrong word, and a century of readers inherited the mistake. (This will matter again on Day 4, when we ask how to make "best explanation" precise using probability.)
The shape of a great misnomer
Holmes is not alone. We say a doctor "diagnoses" — that's abduction, reasoning from symptoms to the disease most likely to produce them. A mechanic listening to an engine, a detective at a crime scene, a scientist staring at an anomalous reading: all abducting, all leaping to the explanation that would render the strange ordinary. Even this sentence relies on it — you're inferring a mind behind these words because that's the best explanation for their orderly arrangement, not because a theorem forces it. Abduction is the water we swim in; we just rarely call it by name.
The distinction everyone fumbles
Valid is not the same as true
Inside the deductive engine lives the single most misunderstood idea in all of logic, and getting it straight is worth more than a dozen memorized fallacies. It is the difference between validity and soundness.
An argument is valid when its form guarantees that true premises would force a true conclusion. Validity is a property of the shape, not the content. The Internet Encyclopedia of Philosophy puts it cleanly: an argument is valid "if and only if it takes a form that makes it impossible for the premises to be true and the conclusion nevertheless to be false." Soundness asks for more — an argument is sound only if it is valid and all its premises are actually true.
Here is the part that trips people: a valid argument can have a wildly false conclusion. Watch.
All birds can fly. A penguin is a bird. Therefore, a penguin can fly.
The form is flawless — "All M are P; s is M; therefore s is P," the very mould Socrates was poured into. If the premises were true, the conclusion would have to follow. So the argument is perfectly valid. It is also, obviously, unsound, because the first premise is false: not all birds fly. Validity certifies the plumbing; soundness asks whether you also pumped in clean water. A valid argument with a false premise is a beautifully engineered pipe carrying sewage.
This is not hair-splitting. It is the working principle behind reductio ad absurdum, one of the sharpest tools in mathematics: to prove a premise false, assume it, reason validly to a conclusion you know is false, and the falsehood flows backward to indict the premise. The whole technique depends on a valid argument deliberately producing a false conclusion. Validity is the carrier; truth is the cargo; learn to track them separately and a fog lifts from every argument you'll ever read.
When the form breaks
The two fallacies hiding in every "if"
If valid forms are the safe paths, fallacies are the trapdoors that look just like them. The most treacherous live in conditional reasoning — statements of the form "if P, then Q" — because the broken versions sit one letter away from the sound ones.
The two valid moves are old friends. Modus ponens: if P then Q; P is true; therefore Q. Modus tollens: if P then Q; Q is false; therefore P is false. Both are airtight. Now meet their evil twins.
Affirming the consequent runs: if P then Q; Q is true; therefore P. It grabs the wrong end. "If someone lives in San Diego, they live in California. Joe lives in California. Therefore Joe lives in San Diego." But California is large; Joe could be in Sacramento. The conclusion might be true, which is exactly what makes the fallacy so seductive — it sometimes lands the right answer for no good reason, and a true conclusion reached by a broken argument is the Gettier trap from Day 1 wearing a logician's coat.
Denying the antecedent is its mirror: if P then Q; P is false; therefore Q is false. "If it's raining, the ground is wet. It isn't raining. Therefore the ground isn't wet." Sprinklers, dear reader. Burst pipes. A spilled bucket. Knocking out one cause does not knock out the effect, because effects can have more than one cause.
There's a teaching classic that makes the structure unforgettable: If an animal is a dog, it has four legs. This animal has four legs. Therefore it is a dog. Cats, horses, and tables object. The absurdity is the point — it's the same broken form as the San Diego argument, just with the silliness turned up so you can see the gears slip. (Eugène Ionesco built an entire scene of his play Rhinoceros on exactly this fallacy, a Logician gravely proving that a cat with four legs must be a dog.)
These are formal fallacies — broken shapes. Their cousins, the informal fallacies, are flaws not in form but in content: post hoc ergo propter hoc (the rooster crows, the sun rises, therefore the rooster summons the dawn), the ad hominem, the equivocation that quietly swaps a word's meaning mid-argument. Formal fallacies you catch by checking the skeleton; informal ones you catch by reading what the words actually do.
Interactive · test the form, not the words
The Inference Inspector
Pick a conditional argument form. The machine doesn't care what the sentences say — only whether the shape guarantees the conclusion. Flip between the two valid moves and their two notorious impostors, then load a real-world example to feel why the broken ones fool us.
Dress it in real words
Reference table
The Inference Inspector
Conditional arguments can be sorted by form before their content is judged.
| Form | Pattern | Verdict | Why |
|---|---|---|---|
| Modus ponens | If P then Q; P; therefore Q | Valid | Affirming the sufficient condition forces the consequent. |
| Modus tollens | If P then Q; not-Q; therefore not-P | Valid | If Q must follow from P, the absence of Q rules P out. |
| Affirming the consequent | If P then Q; Q; therefore P | Invalid | Q may have other causes: Joe can live in California without living in San Diego. |
| Denying the antecedent | If P then Q; not-P; therefore not-Q | Invalid | Removing one sufficient cause does not remove every route to Q: sprinklers can wet the ground. |
The lineage
How logic became mathematics
The machinery you've been using has a deep history, and it bends in a surprising direction: over twenty-three centuries, the study of good argument slowly turned into a branch of algebra. The story has four landmarks.
Aristotle (4th century BCE) built the first formal system in his Prior Analytics. His genius was to use letters as placeholders — "all A are B" — and so to study argument forms apart from their content. This is term logic: it relates terms like "man" and "mortal." Medieval logicians lovingly catalogued the valid syllogistic moods with mnemonic names — Barbara, Celarent, Darii. The names are codes, not people: their vowels mark proposition types, where A means "all S are P," E means "no S are P," I means "some S are P," and O means "some S are not P." So Barbara is AAA, Celarent is EAE, and Darii is AII; Barbara, for example, means all M are P; all S are M; therefore all S are P. For nearly two thousand years, this was logic.
The Stoics, above all Chrysippus (c. 279–206 BCE), built a second, parallel logic that history nearly lost. Where Aristotle related terms, the Stoics related whole propositions with connectives we still use daily: if…then, and, or, not. Chrysippus laid out five "indemonstrables" — basic inference schemata, the first of which ("if the first then the second; but the first; therefore the second") is precisely modus ponens. This is propositional logic, the ancestor of the logic inside every computer chip. The Stoics arguably had a truth-functional grasp of the connectives — understanding "or" by when the whole is true given its parts — two millennia before it was rediscovered. The 20th-century logician Jan Łukasiewicz startled scholars by arguing Stoic logic was not Aristotle's poor cousin but "an achievement of equal rank." Then it was buried for ages while Aristotle reigned — a reminder that intellectual history is not a tidy relay race.
George Boole snapped the two traditions onto a new track. In An Investigation of the Laws of Thought (1854), he did something audacious: he treated logical reasoning as calculation. Let 1 be the universe and 0 be nothing; let multiplication be "and," addition be "or." Suddenly the laws of valid inference looked like the laws of algebra. "We ought no longer to associate Logic and Metaphysics," Boole declared, "but Logic and Mathematics." His book sold modestly and puzzled contemporaries. Only decades later, when Claude Shannon noticed in 1937 that Boole's two-valued algebra described electrical switching circuits exactly, did Boolean algebra become the literal foundation of digital logic. Every AND-gate in the device you're reading this on is a sentence of Chrysippus, rendered in silicon.
Gottlob Frege delivered the largest leap since Aristotle. His slim, forbidding Begriffsschrift ("concept-script," 1879) introduced the quantifier — the formal "for all" (∀) and "there exists" (∃) — and with it predicate logic. Aristotle's term logic choked on arguments like "every horse is an animal, therefore every head of a horse is the head of an animal"; Frege's machinery handled it and vastly more, analyzing propositions as functions fed with arguments. It is often called the finest single book in the history of symbolic logic. There's a tragic coda: Frege dreamed of reducing all of arithmetic to pure logic, and just as the second volume went to press, a young Bertrand Russell sent him a letter containing a paradox — the set of all sets that don't contain themselves: does it contain itself or not? Either answer contradicts itself. Frege's grand foundation cracked. But his logic survived the wreck and became the modern symbolic logic we still teach. (The ghost of that paradox, and the limits it hinted at, will haunt us on Day 28, when Gödel proves no formal system can be everything mathematicians hoped.)
The debate
Is logic discovered or invented?
Here is a question that sounds like a parlor game and turns out to cut very deep. The bedrock laws — identity (A is A), non-contradiction (not both A and not-A), excluded middle (either A or not-A, no third option) — feel utterly inescapable. But where do they live? Are they features of reality, woven into the universe whether or not minds exist? Features of thought, the unavoidable grammar of any thinker? Or human conventions, real and binding but ultimately chosen, like the rules of chess?
Logical realism
discoveredThe laws are objective, mind-independent structures of the world. We don't legislate non-contradiction any more than we legislate the prime numbers — we find it. Logic is read off reality.
Psychologism
laws of thoughtThe laws describe how minds must operate — a branch of psychology. Frege and Husserl attacked this fiercely: logical truths are exact and a priori, while psychology is empirical and fuzzy.
Conventionalism
inventedThe laws are stipulations we adopt because they're useful — binding once chosen, but not handed down by the cosmos. Curiously rare as a fully worked-out position, despite its close kinship to moral anti-realism.
Revisability
empirical?Quine and Putnam floated the radical thought that even logic might be revised for empirical reasons — that quantum mechanics could push us toward a non-classical logic, much as relativity pushed us to non-Euclidean geometry.
That last box is the hinge of today's frontier. For most of history "the laws of thought" seemed untouchable — to question them was to saw off the branch you sat on. But the twentieth century produced rigorous, working alternative logics, systems that quietly drop one of the sacred laws and keep functioning. Once you've seen those alternatives do real labor, the grand metaphysical question softens into something more practical and, frankly, more interesting: not "which logic is True?" but "which logic is the right tool for this job?" Let's go meet the alternatives.
The frontier · 2026
Three live edges — and the hype filter
Every day in this course ends at the research frontier, with each claim tagged for how much weight it can bear. Logic's frontier is unusually concrete: it runs on real computers, checks real proofs, and has lately collided with artificial intelligence in ways that demand a careful eye.
The logics that break the rules — on purpose
"Classical" logic is not the only consistent option; it's one settled point in a landscape of alternatives, each built by surrendering a law most people thought non-negotiable.
Intuitionistic logic drops the law of excluded middle. Pioneered by L.E.J. Brouwer and formalized by Arend Heyting in the 1920s–30s, it insists a statement counts as true only if you can construct a proof of it. You may not assert "A or not-A" for free — you must prove one side. The motivating example is sharp: excluded middle would let you cheerfully assert, for any computer program, "it halts or it doesn't" — yet (as we'll see on Day 27) no general method decides halting, so there's no construction backing the claim. Intuitionism says: then don't assert it. This sounds like philosophical fastidiousness until you learn where it leads — straight into the heart of computer science, via a correspondence so beautiful it gets its own box below.
Paraconsistent logic drops explosion. In classical logic a single contradiction is apocalyptic: from "P and not-P" you can derive literally anything (the principle ex contradictione quodlibet) — one inconsistency and the whole system goes up in flames. Paraconsistent logics refuse this, letting you reason sensibly even when some contradiction has crept in — useful for large databases, legal codes, or any messy body of information that's locally inconsistent but not therefore worthless. The stronger philosophical cousin, dialetheism — Graham Priest's view that some contradictions are actually true, like the Liar sentence "this sentence is false" — is far more controversial. Keep them separate: you can adopt a paraconsistent logic (a technical choice about explosion) without being a dialetheist (a metaphysical claim about true contradictions). The first is a tool; the second is a worldview.
Fuzzy logic drops the two-value restriction entirely. Lotfi Zadeh (1965) let truth slide along the whole interval from 0 to 1 to handle vagueness — "the water is warm" is 0.7 true — building on the many-valued logics of Łukasiewicz from the 1920s. It runs in control systems and appliances. And modal logic — the logic of necessity and possibility (□ and ◇) — together with carefully chosen temporal logics underpins the formal verification of hardware and software: specific fragments are expressive enough to say useful things while remaining decidable enough for model checking. These aren't museum pieces. They're the working logics of the modern technical world.
The bridge · propositions as types
The deepest reason intuitionistic logic matters is the Curry–Howard correspondence: in suitable formal systems, propositions correspond to types and proofs correspond to programs. Proving a theorem can be treated as constructing the program-like object that inhabits its type — and vice versa.
This is why several proof assistants below are built on type-theoretic foundations — and why logic and computation, one of our five threads, are not neighbors but the same country seen from two sides. (Picked up on Days 27–29.)
Proof at zero tolerance: the rise of the proof assistant
Aristotle's dream was a chain of reasoning so tight that no one could doubt it. Twenty-three centuries later, that dream has a software implementation. A proof assistant is a program in which every logical step must pass a mechanical check; nothing is accepted on authority, intuition, or "clearly." The leading systems include Lean (now Lean 4), Rocq (the proof assistant formerly named Coq, renamed in 2025), Agda, and Isabelle/HOL. Lean, Rocq, and Agda live in the type-theoretic family; Isabelle/HOL is based on classical higher-order logic. Same ambition, different foundations.
Lean's community-built library, mathlib, is one of the largest unified formalizations of mathematics ever assembled: more than 278,000 theorems and 132,000 definitions when checked in June 2026, growing continuously, and covering 84 of the 100 problems on a famous "formalize these" challenge list. This is not a toy. Consider what it has already verified:
- 2022 · completedThe Liquid Tensor Experiment. In December 2020, Fields Medalist Peter Scholze challenged the world to verify a theorem from his "condensed mathematics" that he himself wasn't fully sure of. A team led by Johan Commelin and Adam Topaz did it in Lean, finishing on 14 July 2022. A working mathematician used a machine to gain confidence in a proof too intricate for comfortable human refereeing — exactly the point.
- 2023 · completed in 3 weeksThe Polynomial Freiman–Ruzsa conjecture. Days after Tim Gowers, Ben Green, Freddie Manners, and Terence Tao posted a proof of this additive-combinatorics result, Tao launched a Lean project to formalize it — and announced the dependency graph "completely covered in a lovely shade of green" three weeks later. Formalization keeping pace with research, nearly in real time.
- 2024–25 · completedThe Equational Theories Project. Tao's collaborative experiment (launched September 2024) to settle the implication relation among 4,694 algebraic laws — 22,033,636 ordered pairs if you include each law's trivial implication of itself, or 22,028,942 nontrivial graph edges — combining human proofs, automated provers, AI, and Lean verification across 50+ contributors. It finished in just over 200 days: a new model of massively collaborative, machine-checked mathematics.
- 2024–2029 · in progressFermat's Last Theorem. Kevin Buzzard's EPSRC-funded project (launched April 2024, Imperial College London) to formalize FLT — not the original Wiles proof but a modern route. Buzzard is "quietly confident" of reducing it to 1980s-known results, but frank that the whole thing is "at least a 5 year project." Not yet done — the honest status is a work in progress, the last of those 100 challenge problems still open.
And the certainty reaches beyond pure mathematics into systems lives depend on. CompCert is a C compiler proved correct in Rocq; a celebrated bug-hunting study spent roughly six CPU-years trying to make it emit wrong code and failed — "the only compiler we have tested for which Csmith cannot find wrong-code errors" — while finding the usual swarm of bugs in GCC and LLVM. seL4 is the first operating-system microkernel with a full machine-checked proof of functional correctness (in Isabelle/HOL): under its stated assumptions, the C implementation refines the formal specification, so whole classes of crashes and unsafe behaviors are ruled out by theorem rather than hope. These are not ordinary promises; they are conditional theorems about software. This is what logic, mechanized, can do — and it is solidly established.
When AI met the proof checker
The newest and noisiest edge is the collision of machine learning with formal proof — and it is exactly where the hype filter earns its keep, because the headlines and the reality have drifted apart.
The genuine milestone first. In July 2024, DeepMind's AlphaProof, paired with AlphaGeometry 2, solved 4 of 6 problems at the International Mathematical Olympiad, scoring 28 points — the top end of the silver-medal category, one point below the gold threshold of 29. It even cracked the fearsome Problem 6, which only 5 of roughly 600 human contestants fully solved. The methodology was published online in Nature on 12 November 2025, with the version of record appearing in 2026. Here's the design fact that separates it from chatbot bluster: AlphaProof works inside Lean. It auto-formalized about a million natural-language problems into ~80 million formal Lean statements, then trained itself in an AlphaZero-style loop where Lean checks every step. As DeepMind put it, there are "no hallucinations to worry about" — because a hallucinated step simply fails to compile. The neural net supplies creative search; the proof assistant supplies ground truth. That marriage is real and important. established
In July 2025 the bar rose again: both DeepMind (a Gemini "Deep Think" model) and OpenAI reported gold-medal scores — 5 of 6 problems, 35 points — and, strikingly, did it working end-to-end in natural language within the time limit, not in Lean. DeepMind's result was officially certified by the IMO; OpenAI's was graded internally. Genuinely impressive. But here is where you deploy the calibration instinct from Day 1:
- "Gold medal" is a score, not a coronation. These are competition problems — a narrow, time-boxed slice of mathematics with known-to-exist short answers. They are not open research questions, and per the official 2025 results, 26 human contestants still outscored both AI systems.
- Dropping Lean is a trade, not a free upgrade. The 2024 silver was formally verified — guaranteed correct by machine. The 2025 natural-language gold was human-graded, which means we're back to trusting prose that could harbor a subtle gap. More general, less certain. Don't let "gold beats silver" hide that the epistemic ground shifted.
- It is expensive and narrow. Each hard 2024 problem took two to three days of computation, and problems were hand-translated into Lean for the competition. This is not a general mathematical mind.
And the claim to retire most firmly: AI has not "solved mathematics" or made mathematicians obsolete. hype No AI has independently proven a famous open conjecture and had it accepted as a landmark. Reports of theorem-proving agents finding small Lean proofs or helping close narrow formalization tasks are intriguing, but they are early, scoped, and not yet a substitute for accepted research mathematics — the kind of thing to file under promising hint and revisit, not to trumpet. The real revolution is quieter and more durable than the headlines: a 2,300-year-old standard — a proof is a chain no one can doubt — has finally been handed to a machine that enforces it without mercy, and AI is learning to search within those unforgiving rails. (A theme we'll chase properly across Days 138–145.)
A note on fabricated sources
This curriculum's hype filter includes a rule worth stating: discard any citation to a future-dated preprint identifier. Search results in this space are littered with confident-looking references to papers that don't exist yet. Every milestone above is traced to a real, dated, primary source — a published Nature paper, an official competition result, a named researcher's own announcement. When a claim about AI and mathematics can't be traced that way, the right response is not excitement but suspicion.
Open questions
What's genuinely unsettled
Twenty-three centuries in, the study of valid inference still leaves real questions wide open:
- Is there one true logic, or many? Once intuitionistic, paraconsistent, and fuzzy logics all do useful work, "the correct logic" starts to look less like a fact about the universe and more like a choice of tool — but pluralists and monists are still genuinely at odds.
- Discovered or invented? Are the laws of logic read off reality, baked into any possible mind, or adopted by convention? And could empirical physics ever force a revision, as Putnam suspected?
- What is abduction, exactly? Is "inference to the best explanation" a real third mode, or dressed-up induction? Even whether Peirce meant it as inference-to-best-explanation (versus mere hypothesis-generation) is debated among his scholars.
- Can mechanized proof change what mathematics is? If a result is true but only a computer has checked the proof, has anyone understood it? Does a verified-but-opaque proof carry the same value as an illuminating human one?
- And the question that will stalk the AI block: when a machine outputs a true, well-supported theorem, does it know anything — or is it the ultimate Gettier case from Day 1, right for reasons that have nothing to do with comprehension? (Days 138–145.)
◆ The day in three sentences
- Big idea
- Reasoning comes in three engines with three different warranties — deduction preserves truth but adds nothing, induction generalizes but can be broken by the next case, and abduction leaps to the best explanation — and inside deduction, validity (good form) is a wholly separate thing from soundness (good form plus true premises).
- Best analogy
- Sherlock Holmes's "deductions" are really abductions — the best explanation of the clues, not a guaranteed conclusion — and a valid-but-unsound argument is a beautifully built pipe carrying sewage.
- Live controversy
- Whether logic is discovered or invented (and whether there's one true logic or a toolkit of them), now sharpened by a real frontier where proof assistants like Lean verify cutting-edge mathematics at zero tolerance and AI has reached medal-level — but emphatically has not "solved mathematics."
Threads today › computation (Curry–Howard: proofs correspond to programs; Boolean algebra in silicon; proof assistants) · information (formalization makes a proof's content machine-checkable) · emergence (massively collaborative proof settling about 22 million implication relations) — with deduction and induction tying back to Day 1 and Day 2.
Tomorrow → Day 04
Probability as Extended Logic
Today the unreliable engine was induction, and abduction left us needing a way to say which explanation is best. Tomorrow we tame both with numbers. Probability turns out to be not a separate subject from logic but its natural extension to partial belief — and the Monty Hall problem will show how badly our intuitions misfire, and how Bayes' theorem sets them right. Bring today's distinction between airtight and merely-plausible inference; you're about to learn the calculus of the merely plausible.
Sources
Sources & further reading
- "Validity and Soundness." Internet Encyclopedia of Philosophy (accessed 2026). iep.utm.edu/val-snd
- "Deductive and Inductive Arguments." Internet Encyclopedia of Philosophy. iep.utm.edu/ded-ind
- Douven, I. "Abduction." Stanford Encyclopedia of Philosophy (rev. 2021). plato.stanford.edu/entries/abduction
- "Aristotle's Logic." Stanford Encyclopedia of Philosophy. plato.stanford.edu/entries/aristotle-logic
- Bobzien, S. "Ancient Logic." Stanford Encyclopedia of Philosophy. plato.stanford.edu/entries/logic-ancient
- Boole, G. (1854). An Investigation of the Laws of Thought. London: Walton & Maberly. See "George Boole, The Laws of Thought," PhilPapers. philpapers.org/rec/BOOTLO-4
- "Origins of Boolean Algebra in the Logic of Classes." Mathematical Association of America (Convergence). old.maa.org
- "Frege's Logic." Stanford Encyclopedia of Philosophy. plato.stanford.edu/entries/frege-logic
- "Intuitionistic Logic." Stanford Encyclopedia of Philosophy. plato.stanford.edu/entries/logic-intuitionistic
- Priest, G., Berto, F. & Weber, Z. "Dialetheism" and "Paraconsistent Logic." Stanford Encyclopedia of Philosophy. plato.stanford.edu/entries/dialetheism
- "Fuzzy logic." Wikipedia (accessed 2026). en.wikipedia.org/wiki/Fuzzy_logic
- Garson, J. "Modal Logic." Stanford Encyclopedia of Philosophy. plato.stanford.edu/entries/logic-modal
- "Curry–Howard correspondence." Wikipedia (accessed 2026). en.wikipedia.org/wiki/Curry–Howard_correspondence
- "Mathlib statistics." Lean community (accessed June 2026). leanprover-community.github.io/mathlib_stats.html
- "100 theorems in Lean." Lean community (accessed June 2026). leanprover-community.github.io/100.html
- Commelin, J. & Topaz, A. et al. "Liquid Tensor Experiment." Lean community blog (completion 14 July 2022); Scholze's original challenge (Dec 2020). leanprover-community.github.io
- Tao, T. "Formalizing the proof of PFR in Lean4." terrytao.wordpress.com (Nov 2023). Gowers, Green, Manners & Tao, "On a conjecture of Marton," Annals of Mathematics (2025). terrytao.wordpress.com
- Tao, T. et al. "The Equational Theories Project." Project announced Sept 2024; retrospective paper Dec 2025 (arXiv:2512.07087). teorth.github.io/equational_theories
- Buzzard, K. "Fermat's Last Theorem project." Lean community blog (launch 30 April 2024); EPSRC grant EP/Y022904/1 (2024–2029), Imperial College London. leanprover-community.github.io
- Leroy, X. et al. "CompCert" — a formally verified C compiler. Yang, Chen, Eide & Regehr, "Finding and Understanding Bugs in C Compilers," PLDI (2011). compcert.org
- Klein, G. et al. (2009). "seL4: Formal Verification of an OS Kernel." SOSP '09. sel4.systems
- "AI achieves silver-medal standard solving International Mathematical Olympiad problems." Google DeepMind blog (25 July 2024). deepmind.google
- Hubert, T., Mehta, R., Sartran, L. et al. (2026). "Olympiad-level formal mathematical reasoning with reinforcement learning." Nature 651: 607–613. doi:10.1038/s41586-025-09833-y. nature.com/articles/s41586-025-09833-y
- "Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the IMO." Google DeepMind blog (July 2025). deepmind.google
- "66th IMO 2025." International Mathematical Olympiad. imo-official.org/editions/2025 and individual results
- "Our First Proof submissions." OpenAI (2026). openai.com/index/first-proof-submissions
- "Philosophy of logic" & "Logical realism." Wikipedia / Stanford Encyclopedia of Philosophy (accessed 2026). plato.stanford.edu/entries/logical-pluralism
End of Day 03 · 177 descents remain