Homotopy type theory with the univalence axiom of Voevodsky provides both a new logical foundation for mathematics (Univalent Foundations) and a formal language usable with computers for checking the proofs mathematicians make daily. As a foundation, it replaces set theory with a framework where sets are defined in terms of a more primitive notion called "type". As a formal language, it encodes the axioms of mathematics and the rules of logic simultaneously, and promises to make the extraction of algorithms and values from constructive proofs easy. With a semantic interpretation in homotopy theory, it offers an alternative world where the proofs of basic theorems of mathematics can be formalized with minimal verbosity and verified by computer.

As a relative newcomer to the field, I will survey these recent developments and sketch the basic concepts for a general mathematical audience.

In this talk, we will discuss Noncommutative Poisson Structure which was introduced by Crawley-Boevey and how it fits nicely with Kontsevich-Rosenberg principle. We will also give some examples. If time allows, we will also discuss its relation to Van den Bergh's Double Poisson Algebras.

A few years ago I gave a Pizza Seminar talk where I showed how to regularize an infinite sum like \( 1+2+3+4+5+\cdots \) and show that it is equal to \( \frac{-1}{12} \). In this talk I shall discuss a multiplicative version and show how one can regularize infinite products like \( 1.2.3.4.\cdots \). This topic is intimately related to Riemann's zeta function and its analytic continuation and special values. Some tools of classical analysis like Euler-Maclaurin summation formula will be introduced and used extensively in my talk.

I will discuss universal Toda brackets due to Sagave. They are Mac Lane cohomology classes that determine Toda brackets in certain stable homotopy theories and provide an obstruction theory to the problem of realizing $\pi_* R$-modules as $R$-modules for a ring spectrum $R$.

Since creation of quantum groups theory numerous attempts to elaborate an appropriate corresponding differential calculus were undertaken. Recently, a new type of noncommutative geometry has been obtained this way. Namely, we have succeeded in introducing the notions of partial derivatives on the enveloping algebras U(gl(m)) and constructing the corresponding de Rham complexes. All objects arising in our approach are deformations of their classical counterparts. In my talk I plan to introduce some basic notions of the Quantum Groups theory and to exhibit possible applications of this type Noncommutative Geometry to quantization of certain dynamical models.