Yoshua Bengio is Professor in the Computer Science and Operations Research departments at U. Montreal, founder and scientific director of Mila and of IVADO. He is a Fellow of the Royal Society of London and of the Royal Society of Canada, has received a Canada Research Chair and a Canada CIFAR AI Chair and is a recipient of the 2018 Turing Award for pioneering deep learning, is an officer of the Order of Canada, a member of the NeurIPS advisory board, co-founder and member of the board of the ICLR conference, and program director of the CIFAR program on Learning in Machines and Brains. His goal is to contribute to uncovering the principles giving rise to intelligence through learning, as well as favour the development of AI for the benefit of all.

Timothy Gowers is the holder of a chair in combinatorics at the Collège de France, and a fellow of Trinity College, Cambridge. He was awarded the Fields Medal in 1998 for his valuable contributions in combinatorics and functional analysis and by finding new connections between these two areas of mathematics. He is also interested in the idea of extreme human-oriented automated theorem proving which aims to integrate the top-down approach found in human reasoning with the bottom-up process of machine calculations.

Mateja Jamnik is Professor of Artificial Intelligence at the Department of Computer Science and Technology of the University of Cambridge, UK. She is developing AI techniques for human-like computing - she computationally models how people solve problems to enable machines to reason in a similar way to humans. She combines AI reasoning with machine learning techniques to apply them to medical data to advance personalised cancer medicine, and to education to personalise tutoring systems. Mateja is passionate about bringing science closer to the public and engages frequently with the media and public science events. Her active support of women scientists was recognised by the Royal Society which awarded her the Athena Prize. Mateja has been advising the UK government on policy direction in relation to the impact of AI on society.

Jay McClelland is the Lucie Stern Professor in the Psychology Department and Director of the Center for Mind, Brain, Computation and Technology at Stanford University. He is best known for his work in laying the foundations of the connectionist approach. In recent years, his lab has begun exploring the domain of mathematical cognition, in particular, the various kinds of mathematical concepts and reasoning abilities employed by humans, including the grounding of symbols in visual diagrams, the numerical sense of humans, and others.

Alison Pease is a senior lecturer in the School of Science and Engineering at the University of Dundee. Her research is concerned with investigating patterns of collaboration, reasoning and discovery, and incorporating findings into computational systems. She works mostly in mathematics, and believes that this will help us to close the gap between machine and human mathematics, both enhancing interaction between mathematicians and computers, and enabling machines to automatically generate interesting mathematics. She also apply these ideas to scientific domains, and other areas including music, poetry and health.

Stanislas Polu is a research engineer at OpenAI working on the study of generative language models applied to automated theorem proving. He is notable for his work called GPT-f which is the first large-scale language model for the MetaMath and Lean theorem provers.

Markus Rabe is a researcher in automated reasoning. He is a member of the N2Formal team at Google Research, which attempts to build a bridge between logic and natural language using deep neural networks. Before joining Google, Markus was a postdoc at UC Berkeley, and obtained his PhD at Saarland University.

Christian is the lead of the N2Formal team at Google Research. He is known for the Inception neural architecture, for co-inventing batch normalization, and for many more contributions to AI. Since 2016 he and his group have been focusing on AI and mathematics.

Josef Urban is a Principal Researcher at the Czech Institute of Informatics, Robotics and Cybernetics (CIIRC) of the Czech Technical University in Prague where he is heading the ERC-funded project AI4REASON. His interests include Automated Reasoning, Formal Verification and Machine Learning. In particular, he is interested in development of combined inductive/learning and deductive/reasoning "strong AI" methods and systems over large formal (fully semantically specified) knowledge bases. Examples are large corpora of formally stated definitions, theorems and proofs in mathematics, software verification and related fields. He has made such corpora available to the AI methods, created the first benchmarks, and developed first approaches and systems combining learning and reasoning over such corpora in various feedback loops. The systems developed by him and his colleagues have won several competitions and the methods today assist formal verification in proof assistants. He has also co-developed first learning/reasoning systems for automated formalization of informal mathematics, and co-founded the conference on Artificial Intelligence and Theorem Proving (AITP). He received his MSc in Mathematics and PhD in Computers Science from the Charles University in Prague, worked as an assistant professor in Prague, and as a researcher at the University of Miami and Radboud University Nijmegen.