Automath (geautomatiseerde wiskunde) was een formele taal die vanaf 1967 door Nicolaas Govert de Bruijn werd ontwikkeld voor het zodanig uitdrukken van complete wiskundige theorieën dat een erin opgenomen automatische bewijschecker de juistheid van deze theorie kon verifiëren. Het Automath-systeem bevatte vele nieuwe ideeën die later werden ove...