Conférences  >  Mathématiques  >  Mathématiques numériques  >  États-Unis

Institute for Computational and Experimental Research in Mathematics

Spheres are the basic building blocks of geometry. More complicated geometric objects can be built by attaching spheres to each other along continuous maps. For many purposes, such constructions depend only on the homotopy classes of these continuous maps. A fundamental problem in algebraic topology is to compute these homotopy classes, i.e., to compute the homotopy groups of spheres. Machines can be used to great effect in the exhaustive computation of these fundamental invariants of homotopy theory. The workshop will study several software packages that are specifically designed for this purpose. Participants will have the opportunity to interact directly with codebases in work groups led by experienced programmers. The workshop will also introduce a variety of projects in homotopy theory that rely on computers.

Tél.: [4018635030];     Email.: info@icerm.brown.edu

Institute for Computational and Experimental Research in Mathematics

3D reconstruction of scenes from image data is a classic problem in computer vision. Interest in this problem is at an all-time high, thanks to a wealth of applications which impact society in powerful ways---augmented reality, autonomous driving, cultural heritage, localization, mapping, and space exploration, to name a few. Some of these applications demand reliability of 3D reconstructions, e.g., for human safety, which translates to difficult and unsolved problems in mathematics. Other applications require efficiency at an ever-increasing scale, which calls for novelty in computational methods. This workshop will bring together experts working at an exciting crossroads where engineering, geometry, and optimization impact 3D reconstruction.

Tél.: [4018635030];     Email.: info@icerm.brown.edu

Institute for Computational and Experimental Research in Mathematics

Higher category theory, also known as ∞-category theory, is now a fundamental area in modern mathematics, playing a crucial role in many areas of science, such as algebraic topology, algebraic geometry, mathematical physics, and theoretical computer science. Despite its importance, it is still known to be very abstract and technical, and hence difficult to learn without direct access to relevant experts. Formalization of mathematics is a modern approach that uses computers to precisely formulate mathematical statements and proofs via proof assistants. Initially formalization helped verify complicated mathematical results, such as the four color theorem or the liquid tensor experiment. However, in recent years proof assistants have also been used to teach mathematics and design exercises.

This workshop aims to teach participants the fundamentals of higher category theory using the proof assistant Rzk. The participants will learn both the classical point of view and the type theoretic point of view in two lecture series, and, in the exercise sessions, will learn how to use the proof assistant Rzk to prove basic higher categorical results.

Tél.: [4018635030];     Email.: info@icerm.brown.edu