Babbage conceives the Analytical Engine
In 1834, Charles Babbage conceived a programmable general-purpose computing engine, later called the Analytical Engine.
AI timeline
How artificial intelligence evolved: from scientific foundations to modern capabilities.
Last published:
Events
Found: 141
Before 1900
The Origins of Artificial Intelligence
For centuries, philosophers, mathematicians, and inventors explored the possibility of creating thinking machines. Advances in formal logic, mechanical computing devices, and early programming concepts laid the foundation for artificial intelligence.
1834
1843
Publication of Ada Lovelace’s notes on the Analytical Engine
In 1843, Ada Lovelace published notes describing a sequence of operations for computing Bernoulli numbers on the proposed Analytical Engine. She also considered operations on other objects whose relationships could be expressed in a suitable formal representation.
1847
Boole publishes The Mathematical Analysis of Logic
George Boole presented an algebraic approach to logic, allowing propositions and arguments to be analyzed through equations.
1879
Frege publishes Begriffsschrift
Gottlob Frege presented a formal language of relations and quantification with an axiomatic calculus. It allowed reasoning with nested quantifiers to be expressed explicitly.
1900–1942
The Mathematical Foundations of Intelligence
Advances in mathematical logic and computation theory established the scientific foundations of AI. Researchers began exploring the capabilities of algorithms, the principles of computation, and the limits of what machines could solve.
1901
Pearson formulates principal component analysis
Karl Pearson formulated principal component analysis (PCA) as approximating data through projections that minimize the sum of squared errors.
1911
The law of effect in Animal Intelligence
In Animal Intelligence: Experimental Studies, Thorndike presented the law of effect: satisfaction or discomfort accompanying or closely following a response changes its likelihood of recurring in the same situation.
1920
Witness functions in Skolem’s proof
In his 1920 paper, Skolem uses functions that select witnesses for each tuple of universally quantified variables in a proof of satisfiability over a finite or countably infinite domain.
1924
Schönfinkel’s paper on eliminating variables is published
In September 1924, Mathematische Annalen published Schönfinkel’s paper on eliminating bound variables using combinators.
1930
Herbrand’s theorem
Herbrand showed that an entailment from a first-order knowledge base can be proved using a finite subset of its ground instances.
Gödel publishes the completeness theorem for first-order logic
Gödel published a proof of completeness for first-order logic: every logically valid formula has a formal proof.
1932
Church published a logical system using lambda notation
Church’s paper “A Set of Postulates for the Foundation of Logic” appeared in Annals of Mathematics. It described a logical system using lambda notation to represent sets.
1935
Gentzen’s calculi and cut elimination
Gerhard Gentzen developed natural deduction and sequent calculus and proved the cut-elimination theorem.
1936
Turing described a universal computing machine
Turing described a machine capable of reading encoded descriptions of other machines and reproducing their computations.
Fisher publishes a seminal paper on discriminant analysis
Fisher used iris data in his work on discriminant analysis and introduced the term discriminant function.
1940
Church formulates simple type theory
In 1940, Alonzo Church presented a formulation of simple type theory with functions as primitive objects and lambda notation as its sole variable-binding mechanism.
1943–1955
The First Models of Artificial Intelligence
Mathematical models of artificial neurons emerge alongside early research into machine learning. Advances in cybernetics and computing technology open new possibilities for creating systems capable of simulating aspects of human thought.
1943
McCulloch and Pitts’s logical model of neural networks
In December 1943, Warren McCulloch and Walter Pitts published a logical account of neural networks. They showed how to construct networks that realize logical expressions under specified conditions.
1949
Hebb’s learning principle in The Organization of Behavior
In The Organization of Behavior (1949), Donald Hebb proposed that a neuron’s repeated or persistent participation in firing another neuron increases its effectiveness in doing so.
Metropolis and Ulam describe the Monte Carlo method
Metropolis and Ulam presented a statistical approach to difficult computations: examining a random sample of trials or trajectories instead of calculating every possibility.
1950
Turing proposes the imitation game
In Computing Machinery and Intelligence, Turing proposed replacing the question “Can machines think?” with a game in which an interrogator judges a machine's written answers.
Shannon describes search and position evaluation for computer chess
Shannon published a chess-program design combining position evaluation with minimax move selection. He also described selective search as a way to reduce enumeration.
1953
Metropolis algorithm published
Metropolis and colleagues described sampling configurations from the Boltzmann distribution through random particle displacements with acceptance or rejection of proposed moves.
1954
Davis implements Presburger's decision procedure
Martin Davis implemented Presburger's decision procedure in a program that performed an automated proof.
The Georgetown–IBM machine translation demonstration
On January 7, 1954, IBM and Georgetown University publicly demonstrated automatic translation of Russian sentences into English on an IBM 701.
Farley and Clark describe a digital simulation of a learning network
In September 1954, B. G. Farley and W. A. Clark published a study of a digitally simulated self-organizing network. Starting from a random initial state, it learned to distinguish two fixed input patterns by changing connection weights.
1955
Prior publishes Diodoran Modalities
Arthur Prior published the first study of his tense logic, introducing future-time operators into propositional calculus.
The Dartmouth proposal on artificial intelligence
The proposal dated August 31, 1955 outlined a shared research program in artificial intelligence. It initiated the 1956 Dartmouth summer research project.
Successful hand simulation of the Logic Theorist method
According to Newell and Simon, the first successful hand simulation of a theorem proof using methods later incorporated into Logic Theorist took place on December 15, 1955.
1956–1973
The Birth of AI as a Scientific Field
Artificial intelligence emerges as a distinct scientific discipline. Early programs capable of logical reasoning, problem-solving, and natural language interaction inspire a wave of optimism about the future of intelligent machines.
1956
Logic Theorist proves theorems on a computer
In 1956, Logic Theorist became a working program for proving theorems in symbolic logic.
Dartmouth Summer Research Project on Artificial Intelligence
In 1956, a small group of scientists gathered for the Dartmouth Summer Research Project on Artificial Intelligence. The meeting was a seminal event in the emergence of AI as a research field.
1958
The NSS chess program and game-tree pruning
Newell, Shaw, and Simon studied a chess program that used a game-tree pruning method.
Formalizing Fermat’s Last Theorem with Claude
AnthropicWhat happened
According to Anthropic, Claude agents worked largely autonomously for 11 days, following an exposition of an existing proof. A comparator check confirmed that the formal statement matched Mathlib’s formulation of the theorem.
Why it matters
The result demonstrates automated formalization of a complex mathematical proof at the scale of millions of lines of machine-checkable code.
Sources
- Formalizing Fermat's Last Theorem
Supporting excerpt
has been using to describe the initial phase of the project runs to 86 pages. Claude completed the proof in 11 days, producing computer-verifiable proofs of 30,300 theorems along the way (using 29,500 in the final proof). Dozens of Claude agents collaborated to define concepts, prove intermediate theorems, and use those theorems to prove ever harder statements. At 13 million lines of Lean code, Claude’s proof is over 5x the size of Mathlib, the principal community library of mathematical proofs
- FLT: Anthropic has beaten me to it
Supporting excerpt
details The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenstein ideal to conclude that no Frey curve can have a point of order . This
- Fermat's Last Theorem in Lean 4
Supporting excerpt
2026 kernel soundness fixes), with Mathlib compiled from source. All 60,475 modules of this repository built, every declaration was checked by the Lean kernel, and the axioms are as above. comparator. leanprover/comparator v4.33.0 checked the build against verification/comparator/Challenge.lean, which states the theorem using only Mathlib. It confirmed that the proved statement and every constant it mentions are identical to the challenge, that no other axiom is used, and that the whole proof, M
Sources last checked: