This workshop is designed to pool the knowledge and experience of a small and select group of experts to produce agreement on a design that will lead the way to implementation of a semantic capture language applicable to all of mathematics.

The Workshop is co-organized by the Wolfram Foundation, the Fields Institute, and the IMU/CEIC working group for the creation of a World Digital Mathematics Library. A grant in support of the workshop has been provided by the Alfred P. Sloan Foundation and logistical support is by the Fields Institute.

With support from:

Background

In the spring 2014, the Committee on Planning a Global Library of the Mathematical Sciences released a comprehensive study entitled "Developing a 21st Century Global Library for Mathematics Research." This report states in its Strategic Plan section, "There is a compelling argument that through a combination of machine learning methods and editorial effort by both paid and volunteer editors, a significant portion of the information and knowledge in the global mathematical corpus could be made available to researchers as linked open data through the DML [Digital Mathematics Library]."

Most recently, at the August 2014 International Congress of Mathematicians in Seoul, a working group was chartered, working under the IMU's Committee on Electronic Information and Communication, that is dedicated to creating a concrete road map for the creation of a World Digital Mathematics Library (WDML) over the next decade and to starting the mathematical community moving down that road.

A particular area that is vital to the success of the WDML is better semantic representation of mathematical results. This includes not only semantically tagging results from the literature, but also placing them in a form that is computer-readable and interpretable while still retaining human readability. Happily, this is an area where new technologies and recent milestones in computable mathematics suggest it is possible to make near-term and significant forward progress.

This inaugural workshop will attempt to lay down the foundations of a prototype semantic representation language for mathematics. Because of the extremely wide scope of mathematics as a whole, the workshop cannot realistically map out the detailed concepts, structures, and operations needed and used in individual mathematical subjects. Ways to best identify and design semantic components for individual disciplines of mathematics will therefore be another important topic for discussion.

As a proof of concept, a small number of concrete mathematical notions will be discussed and developed in more detail at the workshop (possibly including function spaces, random walks, core algebraic structures, the limit concept, and generalizations of the Riemann hypothesis). The representations of prominent and fundamental theorems in these areas that could serve as building blocks for additional mathematical results will be a focus for discussion.

For further information, please visit: www.wolframfoundation.org/programs/computable-archive-of-mathematics.html

Organizers

Ingrid Daubechies, IMU/CEIC
Ian Hambleton, Fields Institute
Patrick Ion, GDML working group
Stephen Wolfram, Wolfram Research

Confirmed Participants

Avigad, Jeremy - Carnegie Mellon University
Beeson, Michael - San Jose State University
Bhargava, Manjul - Princeton University
Blanchette, Jasmin Christian - Inria Nancy – Grand-Est & LORIA
Bosma, Wieb - Radboud Universiteit
Buchberger, Bruno - Johannes Kepler University
Carette, Jacques - McMaster University
Cheb-Terrab, Edgardo - Maplesoft
Daubechies, Ingrid - IMU/CEIC
Davenport, James - University of Bath
Farmer, William - McMaster University
Friedman, Harvey - The Ohio State University
Gerhard, Juergen - Maplesoft
Gonthier, Georges - Microsoft Research Cambridge
Goroff, Daniel - Alfred P. Sloan Foundation
Hales, Tom - University of Pittsburgh
Hambleton, Ian, Fields Institute
Harrison, John - Intel Corporation
Ion, Patrick - GDML working group
Kamareddine, Fairouz - Heriot-Watt University
Kohlhase, Michael - Jacobs University Bremen
Martin-Garcia, Jose - Wolfram Research, Inc.
Matiyasevitch, Yuri - Steklov Institute of Mathematics
Mulnix, James - Wolfram Research, Inc.
Olde Daalhuis, Adri - University of Edinburgh
Pratt, Vaughan - Stanford University
Sato, Masahiko - Kyoto University
Scott, Dana - Carnegie Mellon University
Smirnov, Stanislav - Université de Genève
Trott, Michael - Wolfram Research, Inc.
Urban, Josef - Radboud Universiteit Nijmegen
Wang, Dongming - Beihang University
Watt, Stephen - University of Waterloo
Weisstein, Eric - Wolfram Research, Inc.
Wiedijk, Freek - Radboud Universiteit Nijmegen
Wolfram, Stephen - Wolfram Research
Zhiltsov, Nikita - Kazan Federal University

Schedule

The Workshop will run from February 3-5, 2016 at the Fields Institute, room 230. The workshop format will be a mixture of overview talks with extensive discussion, hands-on design sessions, and panel-like discussions. The planned format consists of blocks each consisting of an overview talk, a design talk, and an open discussion.

Wednesday, February 3

8:00 - 9:00 Breakfast

9:00 - 10:00 Welcome

9:00 - 9:15

Opening Remarks: Ian Hambleton, Ingrid Daubechies, Daniel Goroff, Patrick Ion

9:30 - 10:00

Overview: Michael Trott

10:00 - 10:30

Introductions

10:30 - 10:45 Coffee break

10:45 - 12:15 Stephen Wolfram: What Will it Take to Design a Language for Pure Mathematics?

12:15 - 13:15 Luncheon

13:15 - 14:45 The language of Formal Mathematics

13:15 - 14:00

Jeremy Avigad: Type Theory and Practical Foundations

14:00 - 14:45

Jeremy Avigad: Homotopy Type Theory

14:45 - 15:00 Tea break

15:00 - 16:30 Foundations of a Mathematical Vernacular

15:00 - 15:45

Dana Scott: Formalizing a Calculus of Enumeration Operators

15:45 - 16:30

Fairouz Kamareddine: From Principia to Formalised versus Computerised Maths

16:30 - 18:00 Towards a Mathematical Vernacular I

16:30 - 17:15

Harvey Friedman: An Approach to the Formal Representation of Mathematical Propositions

17:15 - 18:00

Michael Kohlhase: Flexiformal, Pluralistic, Foundation-Independent Representations of Mathematics

18:00 - 18:15 Tea break

18:15 - 19:45 Towards a Mathematical Vernacular II

18:15 - 19:00

Freek Wiedijk: The Structure of Infallibility

19:00 - 19:30

Jose Martin-Garcia: Studies in the Semantic Representation of Differential Geometry

20:00 Conference dinner (offsite)

Thursday, February 4

8:00 - 9:00 Breakfast

9:00 - 10:30 Semantics of mathematical formulas (PANEL)

Edgardo Cheb-Terrab: The Digitizing of Special Functions, Differential Equations, and Solutions to Einstein’s Equations within a Computer Algebra System

Adri Olde Daalhuis: DLMF: Special functions in the 21st century

James Mulnix: Computable mathematical data in the Wolfram Language

10:30 - 10:45 Coffee break

10:45 - 12:15 Learning from Proofs

10:45 - 11:30

Georges Gonthier: Big proofs, little math

11:30 - 12:15

Tom Hales: Lessons from the formalization of the Kepler Conjecture

12:15 - 13:15 Luncheon

13:15 - 14:45 Notations and Meaning (PANEL)

James Davenport: The Meanings of Mathematical Notations

Masahiko Sato: Bootstrapping Mathematics

Dongming Wang: Representation, Management, and Discovery of Geometric Knowledge

14:45 - 15:00 Tea break

15:00 - 16:30 Design Studies of Mathematical Languages

15:00 - 15:45

Wieb Bosma: The Design of the Magma Language

15:45 - 16:30

Roger Germundsson: Language Design for Probability & Statistics

16:30 - 18:00 Design Studies of Mathematical Provers

16:30 - 17:15

John Harrison: HOL Light and Formal Mathematics

17:15 - 18:00

Bruno Buchberger: Semantic Math Languages in the Context of a "Global Math Digital Library": My Personal View

Friday, February 5

8:00 - 9:00 Breakfast

9:00 - 10:00 Building and Using Mathematical Knowledge Libraries

9:00 - 9:45

Josef Urban: Learning Reasoning and Understanding in Mathematics

9:45 - 10:30

Jasmin Christian Blanchette: Hammering towards QED

10:30 - 10:45 Coffee break

10:45 - 12:15 Ontologies and Using Mathematical Structures (PANEL)

Vaughan Pratt: Qualia and the Duality of Sorts and Properties, via Typed Chu Spaces

Nikita Zhiltsov: The OntoMath Ecosystem

Stephen Watt: Putting "Symbolic" into Symbolic Computations

12:15 - 13:15 Luncheon

13:15 - 14:45 Wrap-up and white paper

2:45 - 3:00 Tea break

Additional white paper discussions (as needed)