Main goals
The Isaac Newton Institute programme on Big Proof during the summer of 2017 drew a great deal of interest from mathematicians, philosophers, and computer scientists. In May 2019 a week-long follow-up workshop funded by the Isaac Newton Institute will take place at the International Centre for Mathematical Sciences in Edinburgh. This workshop will take forward a number of the key initiatives from Big Proof:
- Pragmatic foundations for the formalization of mathematical proofs.
- Social processes that support research, exposition, and learning in mathematics.
- Interchange formats and repositories for formal mathematical knowledge
- Scalable proof automation
- Applications of Big Proof technology
OpenDreamKit implication
Michael Kohlhase (FAU) and Florian Rabe (FAU) were invited participants. The former also gave an invited talk.
Event summary
The workshop consisted of 5 days of 1 hour talks and ample discussion. Due to the invite-inly format, a slew of top researchers from computer science, mathematics, and social sciences were present.
Results and impact
The main result of the workshop from the OpenDreamKit perspective was Kohlhase’s presentation of the Math Data initiative developed within OpenDreamKit. Together with OpenDreamKit’s Big Computation theme, these complement and integrate with the Big Proof topic.