Invited Speakers
Makarius Wenzel, Sketis
“Interaction with Formal Mathematical Documents in Isabelle/PIDE”
Isabelle/PIDE has emerged over more than 10 years as the standard Prover IDE to support interactive
theorem proving in Isabelle, with numerous applications in the Archive of Formal Proofs
(AFP). More recently, the scope of PIDE applications has widened toward languages that are
not connected to logic and proof in Isabelle, but taken from a broader repertoire of mathematics
on the computer. The present paper provides an overview of the current status of the PIDE
project and its underlying document model, with built-in support for parallel evaluation and
asynchronous interaction. There is also some discussion of original aims and approaches,
successes and failures, later changes to the plan, and ideas for the future.
Henry Prakken, Utrecht University
“AI Models of Argumentation and Some Applications to Mathematics”
Argumentation is the process of supporting claims with grounds and of defending the thus constructed
arguments against criticism. AI researchers have for more than 30 years studied the
formal and computational modelling of argumentation. This has resulted in increased understanding
of argumentation and in computer tools for supporting human argumentation or
performing artificial argumentation.
At first sight, the rigor of mathematical thinking would be far from the “messy” world of
argumentation. However, inspired by Polya’s and Lakatos’s groundbreaking studies of the
practice of mathematical proof, quite a few scholars have studied “mathematics in action” as a
form of argumentation. Some of that work employs formal and computational tools from AI. In
this talk I will first give an overview of the formal and computational study of argumentation in
AI, and I will then discuss several applications to mathematical modelling and proof.
Sylvain Corlay, QuantStack
Jupyter: From IPython to the Lingua Franca of Scientific Computing
Since its creation in 2011, the Jupyter notebook has exploded in popularity, with a user base growing from thousands to millions. Beyond notebooks, Jupyter is, in fact, a large collection of tools meant to facilitate workflows of researchers from the exploratory analysis to the communication of their results.
In this talk, we will present the main components of the ecosystem, from JupyterLab to the interactive widgets, including Binder and JupyterHub. We will show how they work together to enable the variety of use-cases for which Jupyter is used today.
Then, we will try to show where the project is going in the next few months, and present the latest updates on dashboarding tools, data visualization libraries, and new language backends.
|