The computational content of abstract algebra and analysis

Venue: The event will take place online through the ZOOM platform. To get the access codes please contact the secretary office (phd.maths [at] unitn.it)
Time: 10.15 a.m.

Franziskus Wolfgang Josef Wiesnet - PhD in Mathematics, University of Trento

Abstract:
We discuss several forms of proof interpretation based on examples in algebra and analysis. In particular, we show the construction of algorithms and functions out of proofs. 
The main example in this talk will consider maximal objects and their approximations in various algebraic structures. The existence of maximal objects in algebra often requires Zorn’s lemma. Inspired by Gödel's functional interpretation and methods from proof mining we define approximate explicit maximal objects and show a state-based algorithm which computes them. An application of this approach is the universal Krull-Lindenbaum lemma. 
As second example we consider Zariski's lemma and sketch how a manual construction of an algorithm from a constructive proof works. We give a constructive proof of Zariski's lemma, and use this proof as inspiration to formulate an algorithm and a computational interpretation of Zariski's lemma.
The third example is about program extraction in constructive analysis by using computer assistance. We use coinductively defined predicates to prove that the signed digit representation of real numbers is closed under limits of convergent sequences. From a formal proof in the proof assistant Minlog, the computer generates an algorithm, a soundness theorem and a proof of the soundness theorem corresponding to the convergence theorem out of our formalisation. 
The final example is about proof mining in analysis. We consider a convergence lemma with a classical proof, use techniques of proof mining to get a new lemma with a rate of convergence, and apply the new lemma to various fixed-point theorems for asymptotically weakly contractive maps and their variants.

Supervisor: Peter Schuster