An Unsolvable Problem of Elementary Number Theory Alive
Church's independent proof of the Entscheidungsproblem's undecidability — via the lambda calculus, the formal system every functional language descends from.
Published in the American Journal of Mathematics in April 1936 — months before Turing's paper appeared — Church's proof established that no general decision procedure exists for arithmetic. His tool was the lambda calculus, a notation for function definition and application he had developed with students Stephen Kleene and Barkley Rosser at Princeton.
The paper matters beyond the theorem: it gave computation its first precise formal model. Every functional programming language — Lisp, ML, Haskell, Scheme — is an engineered descendant of Church's notation, and the Church–Turing thesis linking his model to Turing's machine remains the foundation of computability theory.