SMS scnews item created by Catherine Meister at Mon 5 Aug 2024 1332
Type: Seminar
Modified: Mon 5 Aug 2024 1558; Mon 12 Aug 2024 1040
Distribution: World
Expiry: 31 Aug 2024
Calendar1: 16 Aug 2024 0900-1100
CalLoc1: SMRI Seminar Room (A12 Room 301)
CalTitle1: Lean times: The anatomy of a proof assistant
Auth: cmeister@167-179-157-30.a7b39d.syd.nbn.aussiebb.net (cmei0631) in SMS-SAML

Informal Friday Seminar: Bauer -- Lean times: The anatomy of a proof assistant

Abstract: A proof assistant is a program that helps formalize mathematics by automating 
construction of formal proofs and verifying their correctness. It employs a collection 
of programming techniques that seem unfamiliar to a mathematician, but are just
 implementations of methods that mathematicians use in everyday work, but rarely speak 
of them or teach them explicitly.