Title: A proof mining case study on the unit interval
Speaker: Andrei Sipoș (University of Bucharest & IMAR)
Abstract:
In 1991, Borwein and Borwein proved [1] the following: if L>0, f : [0,1] → [0,1] is L-Lipschitz, (xn), (tn) ⊆ [0,1] are such that for all n, xn+1=(1-tn)xn+tnf(xn) and there is a δ>0 such that for all n, tn≤(2-δ)/(L+1), then the sequence (xn) converges.
The relevant fact here is that the main argument used in their proof is of a kind that hasn’t been analyzed yet from the point of view of proof mining, and thus it may serve as an illustrative new case study. We shall present our work [2] on the proof, showing how to extract a uniform and computable rate of metastability for the above family of sequences.
References:
Title: Exponential Diophantine equations over ℚ
Speaker: Mihai Prunescu (University of Bucharest & IMAR)
Abstract:
In a previous exposition [1] we have seen that the solvability over ℚ is undecidable for systems of exponential Diophantine equations. We now show that the solvability of individual exponential Diophantine equations is also undecidable, and that this happens as well for some narrower families of exponential Diophantine equations.
References:
We are pleased to support UNbreakable Romania – the national competition organised for students in the country preparing for a career in cybersecurity.
- The preparation stage will start on April 1 when the registered participants will have at their disposal theoretical and practical resources that will allow them to become familiar with the format and methodology of the contest.
2. The individual contest will take place between May 14-16.
3. The team competition will take place on June 4-6.
At the end of the season, there will be a national #ROEduCyberSkills ranking that will provide an overview of cybersecurity performance in Romania.
Registration is free and is available on the official website: https://unbreakable.ro/inregistrare
Title: Unwinding of proofs
Speaker: Pedro Pinto (TU Darmstadt)
Abstract:
The unwinding of proofs program dates back to Kreisel in the fifties and rests on the following broad question:
“What more do we know if we have proved a theorem by restricted means than if we merely know that it is true?”
This research program has since been dubbed proof mining and has been greatly developed during the last two decades and emerged as a new form of applied proof theory [1,2]. Through the use of proof-theoretical tools, the proof mining program is concerned with the unveil of hidden finitary and combinatorial content from proofs that use infinitary noneffective principles.
In this talk, we set out to give a brief introduction to the proof mining program, focusing on the following points:
- functional interpretations in an introductory way;
- the bounded functional interpretation [3,4];
- a concrete translation example: the metric projection argument.
We finish with a brief discussion of some recent results [5,6].
References:
[1] U. Kohlenbach.
Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg, 2008.
[2] U. Kohlenbach.
Proof-theoretic methods in nonlinear analysis. In M. Viana B. Sirakov, P. Ney de Souza, editor,
Proceedings of the International Congress of Mathematicians – Rio de Janeiro 2018, Vol. II: Invited lectures, pages 61–82. World Sci. Publ., Hackensack, NJ, 2019.
[3] F. Ferreira and P. Oliva.
Bounded functional interpretation.
Annals of Pure and Applied Logic, 135:73-112, 2005.
[4] F. Ferreira.
Injecting uniformities into Peano arithmetic.
Annals of Pure and Applied Logic, 157:122-129, 2009.
[5] B. Dinis and P. Pinto.
Effective metastability for a method of alternating resolvents. arXiv:2101.12675 [math.FA], 2021.
[6] U. Kohlenbach and P. Pinto.
Quantitative translations for viscosity approximation methods in hyperbolic spaces. arXiv:2102.03981 [math.FA], 2021.
Title: Formalizing Gödel’s System T in Lean
Speaker: Horațiu Cheval (University of Bucharest)
Abstract:
In 1958, Gödel introduced his functional interpretation as a method of reducing the consistency of first-order arithmetic to that of a quantifier-free system of primitive recursive functionals of higher type. His work has since enabled other advances in proof theory, notably the program of proof mining. We give a brief overview of Gödel’s System T and then explore a formalization thereof as a deep embedding in the Lean proof assistant.
References:
The students of the Faculty of Mathematics and Computer Science Dragoș Albastroiu (3rd-year, CTI) – captain, Robert Dobre (3rd-year, Computer Science), Mihail Feraru (2nd-year, Computer Science) and Andrei Ciobanu (2nd-year master, Security and Applied Logic) represented the University of Bucharest at the Hack The Box University 2020 Qualifier Round, which took place in November, 19th-22nd, online. In the competition participated teams from universities all around the world, and the team of the University of Bucharest ranked among the best, becoming eligible to remain in the competition.
The Practical Training options for first year SLA students has been posted at the address: https://sla.cs.unibuc.ro/en/practical-training-for-first-year-sla-students/
Organizatorii DefCamp anunță lansarea platformei educaționale CyberEDU. Accesul la această resursă este gratuit.
Universitatea din Bucuresti este acum prezenta pe Hack the Box!
Daca aveti cont pe Hack the Box si vreti sa primiti o invitatie pentru a face parte din echipa de studenti a universitatii, trimiteti user-ul, numele complet, grupa si un e-mail de contact (catre Ruxandra Olimid).
