You are currently browsing the tag archive for the ‘machine assisted proof’ tag.

Just a short post to advertise the workshop “Machine assisted proofs” that will be held on Feb 13-17 next year, here at the Institute for Pure and Applied Mathematics (IPAM); I am one of the organizers of this event together with Erika Abraham, Jeremy Avigad, Kevin Buzzard, Jordan Ellenberg, Tim Gowers, and Marijn Heule. The purpose of this event is to bring together experts in the various types of formal computer-assisted methods used to verify, discover, or otherwise assist with mathematical proofs, as well as pure mathematicians who are interested in learning about the current and future state of the art with such tools; this seems to be an opportune time to bring these communities together, given some recent high-profile applications of formal methods in pure mathematics (e.g, the liquid tensor experiment). The workshop will consist of a number of lectures from both communities, as well as a panel to discuss future directions. The workshop is open to general participants (both in person and remotely), although there is a registration process and a moderate registration fee to cover costs and to restrict the capacity to genuine applicants.