Research Associate

Fellow of St Edmund’s College

Computer Laboratory

15 JJ Thomson Avenue

University of Cambridge

CB3 0FD, UK

ak2110[at]cam[dot]ac[dot]uk

Tel.: (+44)/(0)1223763620
(Office)

I am a mathematician working within the ERC Project ALEXANDRIA led by Professor Lawrence Paulson. I am a member of the Automated Reasoning Group which is a part of the Programming, Logic and Semantics Research Group, at the Computer Laboratory, University of Cambridge , UK.

I was previously (10/2016-9/2017) a Scientific Associate at the Research Group Logic, Department of Mathematics, Technische Universität Darmstadt, Germany, under Professor Ulrich Kohlenbach.

My Erdős number is 4.

Formalization of mathematical proofs with Isabelle ; Automated theorem proving and verification; Mechanisation of mathematics; Intersection of logic and mathematics; (Applied) proof theory, in particular I have been working on proof mining (pen-and-paper extraction of computable bounds from mathematical proofs) applied to proofs in nonlinear analysis, differential equations and fixed point theory; Foundations of mathematics.

PhD (Dr. rer. nat.) in Mathematics, Department of Mathematics , Technische Universität Darmstadt, Germany. The defense of my PhD thesis entitled * ''Proof Mining for Nonlinear Operator Theory: Four Case Studies on Accretive Operators, the Cauchy Problem and Nonexpansive Semigroups'' * under supervision of Prof. Dr. Ulrich Kohlenbach and funded by the International Research Training Group 1529 (Oct. 2013- Sept. 2016) took place on Dec. 21, 2016.

I previously obtained a M.Sc. in Mathematics from the Department of Mathematical Sciences, University of Copenhagen, Denmark (Dec. 2012), a Master de Sciences et Technologies (Mention Physique et Applications) from Université Paris VI (Pierre et Marie Curie), France, and a Diploma from the School of Applied Mathematical and Physical Sciences , National Technical University of Athens, Greece (2009).

- New effective bounds for the approximate common fixed points and asymptotic regularity of nonexpansive semigroups, Journal of Logic and Analysis, vol. 10 (2018).
- Effective rates of convergence for the resolvents of accretive operators , Numerical Functional Analysis and Optimization, vol. 38, issue 12, 1601-1613 (2017).
- Effective asymptotic regularity for one-parameter nonexpansive semigroups (with Ulrich Kohlenbach), J. Math. Anal. Appl. vol. 433, 1883-1903 (2016).
- Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators (with Ulrich Kohlenbach), J. Math. Anal. Appl. vol. 423, 1089-1112 (2015).

- Irrationality criteria for series by Erdős and Straus (with Wenda Li), May 2020.
- Aristotle's Assertoric Syllogistic, Oct. 2019.
- The transcendence of certain infinite series (with Wenda Li), March 2019.
- Octonions, Sept. 2018.
- Irrational rapidly convergent series (with Wenda Li), May 2018.

- SErAPIS: A Concept-Oriented Search Engine for the Isabelle Libraries Based on Natural Language (with Yiannos Stathopoulos and Lawrence Paulson), to appear in the informal proceedings of the Isabelle Workshop 2020 affiliated to IJCAR 2020, (in Virtual Space), June 30, 2020.
- Developing a Concept-Oriented Search Engine for Isabelle Based on Natural Language : Technical Challenges (with Yiannos Stathopoulos and Lawrence Paulson), to appear in the informal Proceedings of the 5th Conference on Artificial Intelligence and Theorem Proving (AITP 2020), Aussois, France, Mar. 22-27, POSTPONED TO Sept. 13-18, 2020.
- Proof mining mathematics, formalizing mathematics, Proceedings of the North American Annual Meeting of the Association for Symbolic Logic, University of Western Illinois, Macomb, Illinois, USA, May 16-19, 2018, the Bulletin of Symbolic Logic, Volume 24, Issue 4, December 2018.
- An invitation to proof mining: two applications in nonlinear operator theory, Proceedings of the 2017 European Summer Meeting of the Association for Symbolic Logic, Logic Colloquium 2017 Stockholm, Stockholm, Sweden, Aug.14-20, 2017, the Bulletin of Symbolic Logic, Volume 24, Issue 2, June 2018.
- Proof mining: An ''effective'' program (even) for ineffective Mathematics, Proceedings of the 11th Panhellenic Logic Symposium, Delphi, July 12-16, 2017 , (Alexandra Soskova, Antonis Kakas, and Nikolaos Papaspyrou eds.).
- New Applications of Proof Mining to Nonlinear Analysis (with Ulrich Kohlenbach) in : Piecha, Thomas; Schröder-Heister, Peter: General Proof Theory. Celebrating 50 Years of Dag Prawitz's "Natural Deduction". Proceedings of the Conference held in Tübingen, 27-29 Nov. 2015.
- Proof-theoretic methods in nonlinear analysis IV: Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators (with Ulrich Kohlenbach) in : Oberwolfach Workshop: Mathematical Logic: Proof theory, Constructive Mathematics (1447), 16-22 Nov. 2014, Report No. 52/2014.

- Invited speaker at the Colloquium Logicum, Konstanz, Germany,
~~Sept. 23-26, 2020~~postponed to March 2021. - Invited speaker at the Big Proof Workshop, Edinburgh, UK, May 27-31, 2019.
- Invited speaker at the Leeds Logic Seminar (8/5/2019), University of Leeds, UK.
- Invited speaker at the 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019), Obergurgl, Austria, Apr. 7-12, 2019.
- Invited speaker at the Third Workshop on Formal Mathematics for Mathematicians (FMM), RISC, Hagenberg, Austria, Aug. 13, 2018.
- '' ALEXANDRIA '' (20/6/2018) Invited speaker at the Logic Seminar, Imperial College London, UK.
- (25/5/2018) Women @ CL Talklet, Computer Laboratory, University of Cambridge, UK.
- "Proof mining mathematics, formalizing mathematics"(17/5/2018) Invited speaker-special session on proof theory North American Annual Meeting of the Association for Symbolic Logic, University of Western Illinois, Macomb, Illinois, USA, May 16-19, 2018.
- "An invitation to proof mining: two applications in nonlinear operator theory"(18/8/2017), Logic Colloquium 2017, Stockholm, Sweden, Aug.14-20, 2017.
- ''Proof Mining for the Fixed Point Theory of Nonexpansive Semigroups''(27/7/2017), Proof, Computation, Complexity 2017 Sixteenth International Workshop, Göttingen, Germany, July 26-27, 2017.
- ''Proof mining: An ''effective'' program (even) for ineffective Mathematics'' (15/7/2017), 11th Panhellenic Logic Symposium, Delphi, Greece, July 12-16, 2017.
- ''Automorphisms of the Calkin algebra under two different set-theoretic hypotheses: an independence result'' (17/5/2017) C*-algebras/Didactics Seminar, TU Darmstadt, Germany.
- ''Proof Mining for Nonexpansive Semigroups'' (4/5/2017), PhDs in Logic IX , Ruhr-University Bochum, Germany, May 2-4, 2017.
- PhD thesis defense: ''Proof Mining for Nonlinear Operator Theory: Four Case Studies on Accretive Operators, the Cauchy Problem and Nonexpansive Semigroups'' (21/12/2016), TU Darmstadt, Germany.
- "New effective bounds for the approximate common fixed points and asymptotic regularity of nonexpansive semigroups " (19/4/2016), IRTG 1529 Seminar, TU Darmstadt, Germany.
- "New Applications of Proof Mining to Nonlinear Analysis" (29/11/2015), General Proof Theory: Celebrating 50 Years of Dag Prawitz's "Natural Deduction", Tübingen, Germany, Nov. 27-29, 2015.
- ''Effective information for abstract Cauchy problems extracted via Proof Mining'' (8/10/2015), SPP 1506, IRTG 1529 and DFG-JSPS Joint International Conference and Autumn School, Darmstadt, Germany, Oct. 5-8, 2015.
- ''Approximate common fixed points and rates of asymptotic regularity for one-parameter nonexpansive semigroups'' (20/7/2015), 11th International Conference on Fixed Point Theory and Applications, Istanbul, Turkey, July 20-24, 2015.
- ''Approximate common fixed points and rates of asymptotic regularity for one-parameter nonexpansive semigroups'' (17/7/2015), Logic Seminar, TU Darmstadt, Germany.
- ''Recent proof mining results for PDE theory and fixed point theory and other ongoing applications of proof theory to analysis'', (15/6/2015), Poster presentation, 10th Panhellenic Logic Symposium , Samos, Greece, June 11-15, 2015.
- ''Proof mining and nonlinear semigroups'' (9/6/2015), IRTG 1529 Seminar, TU Darmstadt, Germany.
- ''First application of proof mining to partial differential equations; rates of convergence and metastability for abstract Cauchy problems generated by accretive operators''(3/3/2015), Constructivism and Computability, JAIST Logic Workshop Series, Kanazawa, Japan, Mar. 2-6, 2015.
- ''Proof-Theoretic Methods in Nonlinear Analysis, Part 4; rates of convergence and metastability for abstract Cauchy problems generated by accretive operators''(20/11/2014), Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics, Mathematical Research Institute Oberwolfach, Nov. 16-22, 2014.
- ''Proof mining and partial differential equations; rates of convergence and metastability for abstract Cauchy problems generated by accretive operators''(7/11/2014), the Sendai Logic Seminar , Tohoku University, Japan.
- ''Proof mining and partial differential equations''(25/4/2014), PhDs in Logic VI, Utrecht, the Netherlands, April 24-25, 2014.
- ''Proof mining for Cauchy problems generated by accretive operators''(27/2/2014), IRTG 1529 Research Seminar "Proof Mining and Nonlinear Analysis", TU Darmstadt, Germany, Feb. 26-28, 2014.
- ''Proof Theory and PDEs''(29/1/2014) ,IRTG 1529 Winter Seminar and Klausurtagung, Chalet Giersch, La Clusaz, France, Jan. 27-31, 2014.
- "Automorphisms of the Calkin algebra under two different set-theoretic hypotheses; An independence result" (21/6/2013), Logic Seminar, TU Darmstadt, Germany.
- "Automorphisms of the Calkin algebra under two different set-theoretic hypotheses; An independence result"(18/12/2012), Master thesis defense, Department of Mathematical Sciences, University of Copenhagen, Denmark.
- "Under Todorcevic's Axiom, all the automorphisms of the Calkin algebra are inner, I, II, III" (15, 22, 29/11/2012), Set Theory and Applications Seminar, University of Copenhagen, Denmark.
- "Under CH, the Calkin algebra has outer automorphisms "(3/10/2012), Set Theory and Applications Seminar, University of Copenhagen, Denmark.

- Kohlenbach, Ulrich: Proof-theoretic methods in nonlinear analysis. Proceedings of the International Congress of Mathematicians, Rio de Janeiro 2018. Vol. II. Invited lectures, 61 --82, World Sci. Publ., Hackensack, NJ, 2018.
- Peng, Weiguang and Yamazaki, Takeshi : Two kinds of fixed point theorems and reverse mathematics. MLQ Math. Log. Q. 63 (2017), no. 5, 454--461.
- Sanders, Sam: The computational content of nonstandard analysis. Proceedings of the Sixth International Workshop on Classical Logic and Computation, 24-40, Electron. Proc. Theor. Comput. Sci. (EPTCS), 2016.
- Leuştean, Laurenţiu and Nicolae, Adriana: Effective results on nonlinear ergodic averages in CAT $(\kappa)$ spaces. Ergodic Theory Dynam. Systems 36 (2016), no. 8, 2580--2601.
- Sipoş, Andrei: Effective results on a fixed point algorithm for families of nonlinear mappings. Ann. Pure Appl. Logic 168 (2017), no. 1, 112--128.
- Setzer, Anton : The use of trustworthy principles in a revised Hilbert's program. Gentzen's centenary, 45-60, Springer, Cham, 2015.
- Leitsch, Alexander: On proof mining by cut-elimination. All about proofs, proofs for all, 173-200, Stud. Log. (Lond.), 55, Math. Logic Found., Coll. Publ., London, 2015.

- Member of the Research Staff Forum at the Computer Laboratory, University of Cambridge .
- Member of the local organisers of the 25th Automated Reasoning Workshop (Cambridge 12-13 Apr. 2018) and of the organising committee of ''PhDs in Logic VIII'' (TU Darmstadt, 9-11 May 2016).
- Research stay at Waseda University, Tokyo, Japan (1/9/2014-10/3/2015) hosted by the Analysis Research group, in connection to the IRTG 1529 . During this time also very briefly visited the Sendai Logic group of Tohoku University and JAIST in Kanazawa.
- Member of the : Association for Symbolic Logic , the British Logic Colloquium , the DVMLG and The Trinity Mathematical Society.
- Doktorandentreff

*At the University of Cambridge:*Supervision for Logic and Proof (Lent Term 2020), (Lent Term 2019), (Lent Term 2018).-
*At TU Darmstadt, Department of Mathematics:*SoSe 2017-Teaching Assistant for Proof Theory, WiSe 2016-2017-Teaching Assistant for Complex Analysis (with Dr. Florian Steinberg), Differential Equations (with Dr. Martin Saal). -
*At the University of Copenhagen, Department of Mathematical Sciences:*Exercise classes for Mathematical Physics (2010-2011, 2011-2012), LaTeX (2011, 2012).

- Colloquium Logicum, Konstanz, Germany,
~~Sept. 23-26, 2020~~postponed to March 2021. - 5th Conference on Artificial Intelligence and Theorem Proving (AITP 2020), Aussois, France,
~~Mar. 22-27~~postponed to Sept. 13-18, 2020. - Isabelle Workshop 2020,(in Virtual Space), June 30, 2020.
- IJCAR 2020,(in Virtual Space), June 29-July 6, 2020.
- The Big Mathematics Initiative, ICMS Edinburgh (in Virtual Space), June 11, 2020.
- 7th Oxbridge Women in Computer Science Conference, Cambridge, UK, Mar. 12, 2020. [POSTPONED]
- 2nd Logipedia Meeting, ENS-Paris-Saclay, Paris, France, Jan. 27-28, 2020.
- Tableaux 2019/ 26th Automated Reasoning Workshop(ARW 2019), London, UK, Sept. 2-3, 2019.
- Big Proof Workshop, Edinburgh, UK, May 27-31, 2019.
- Symposium on AI for Social Good, Cambridge, UK, May 24, 2019.
- 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019), Obergurgl, Austria, Apr. 7-12, 2019.
- The Second Meeting in Ethics in Mathematics (EiM2), Cambridge, UK, Apr. 3-5, 2019.
- The Trinity Mathematical Society Centenary Symposium, Cambridge, UK, Feb. 23, 2019.
- Set Theory in the UK, Cambridge, UK, Feb. 16, 2019.
- Twelfth Annual Cambridge Graduate Conference on the Philosophy of Mathematics and Logic, Cambridge, UK, Jan. 19-20, 2019.
- Mathematical Models and Mathematical Software as Research Data (M3SRD 2018), RISC, Hagenberg, Austria, Aug. 13, 2018.
- Third Workshop on Formal Mathematics for Mathematicians (FMM), RISC, Hagenberg, Austria, Aug. 13, 2018.
- Isabelle Workshop 2018 , Oxford, UK, July 13, 2018.
- 9th International Conference on Interactive Theorem Proving (ITP 2018) , Oxford, UK, July 9-12, 2018.
- Workshop on Proof Complexity (PC 2018), Oxford, UK, July 7-8, 2018.
- 7th International Workshop on Classical Logic and Computation CL&C 18, Oxford, UK, July 7, 2018.
- North American Annual Meeting of the Association for Symbolic Logic, University of Western Illinois, Macomb, Illinois, USA, May 16-19, 2018.
- 25th Automated Reasoning Workshop (ARW 2018), Cambridge, UK, Apr. 12-13, 2018.
- Foundations in Mathematics: Modern Views, Munich, Germany, Apr. 4-7, 2018.
- 5th Oxbridge Women in Computer Science Conference, Cambridge, UK, Mar. 15, 2018.
- Linear Algebra in Isabelle/HOL, University of La Rioja, Logroño, Spain, Nov. 15-17, 2017.
- Autumn school "Proof and Computation", Herrsching, Germany, Sept. 23-26, 2017.
- Logic Colloquium 2017, Stockholm, Sweden, Aug.14-20, 2017.
- Proof, Computation, Complexity 2017 Sixteenth International Workshop, Göttingen, Germany, July 26-27, 2017.
- 11th Panhellenic Logic Symposium, Delphi, Greece, July 12-16, 2017.
- Computer-aided mathematical proof , Isaac Newton Institute for Mathematical Sciences, Cambridge, UK, July 10-14, 2017.
- PhDs in Logic IX , Ruhr-University Bochum, Germany, May 2-4, 2017.
- Colloquium Logicum 2016, Hamburg, Germany, Sept. 10-12, 2016.
- World Congress in Philosophy 2016 , Athens, Greece, July 9-15, 2016.
- PhDs in Logic VIII , TU Darmstadt, Germany, May 9-11, 2016.
- Winter School in Abstract Analysis 2016, Section Set Theory and Topology , Hejnice, Czech Republic, Jan. 30 - Feb. 6, 2016.
- General Proof Theory: Celebrating 50 Years of Dag Prawitz's "Natural Deduction" ,Tübingen, Germany, Nov. 27-29, 2015.
- SPP 1506, IRTG 1529 and DFG-JSPS Joint International Conference and Autumn School, Darmstadt, Germany, Oct. 5-8, 2015.
- 11th International Conference on Fixed Point Theory and Applications, Istanbul, Turkey, July 20-24, 2015.
- Tenth International Conference on Computability, Complexity and Randomness, Heidelberg, Germany, June 22-26, 2015.
- 10th Panhellenic Logic Symposium , Samos, Greece, June 11-15, 2015.
- PhDs in Logic VII, Vienna, Austria, May 14-16, 2015.
- JSPS-NUS Joint Workshop in Mathematical Logic and Foundations of Mathematics, Kanazawa, Japan, Mar. 6-8, 2015.
- Constructivism and Computability, JAIST Logic Workshop Series, Kanazawa, Japan, Mar. 2-6, 2015.
- RIMS Workshop on Proof Theory, Computation Theory and Related Topics , Kyoto, Japan, Dec. 24-26, 2014.
- Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics, Mathematical Research Institute Oberwolfach, Nov. 16-22, 2014.
- Eleventh International Conference on Computability and Complexity in Analysis, TU Darmstadt, Germany, July 21-24, 2014.
- PhDs in Logic VI, Utrecht, the Netherlands, April 24-25, 2014.
- IRTG 1529 Research Seminar "Proof Mining and Nonlinear Analysis", TU Darmstadt, Germany, Feb. 26-28, 2014.
- IRTG 1529 Winter Seminar and Klausurtagung, Chalet Giersch, La Clusaz, France, Jan. 27-31, 2014.
- 9th Panhellenic Logic Symposium , Athens, Greece, July 15-18, 2013.
- 6th Young Set Theory Workshop, Santuario di Oropa, Italy, June 10-14, 2013.
- Workshop on Modal Logic: Modality and Modalities, Roskilde University, Denmark, May 23-24, 2013.
- Workshop on Intensionality in Mathematics, Filosofiska Institutionen, Lund, Sweden, May 11-12, 2013.
- Workshop on Applications to Operator Algebras, The Fields Institute for Research in Mathematical Sciences, Toronto, Canada, Sept. 10-14, 2012.
- Appalachian Set Theory Workshop on C*- algebras, Classification and Descriptive Set Theory, The Fields Institute for Research in Mathematical Sciences, Toronto, Canada, Sept. 8-9, 2012.
- 8th Scandinavian Logic Symposium, Roskilde University, Denmark, Aug. 20-21, 2012.
- Asian Initiative for Infinity (AII) Graduate Summer School, Institute for Mathematical Sciences (IMS), National University of Singapore, June 20-July 17, 2012.

- St Edmund’s College, University of Cambridge
- The Proof Theory Blog
- MathOverflow
- ICMS Edinburgh
- The Archive of Formal Proofs
- Isabelle/HOL Sessions- Library
- Isabelle Repository
- Formalizing 100 Theorems
- Interactive Formal Verification Course Material
- Seminars at the Isaac Newton Institute for Mathematical Sciences
- DPMMS Seminars at the Department of Mathematics, University of Cambridge
- DAMTP Seminars at the Department of Mathematics, University of Cambridge
- The Cambridge University Ethics in Mathematics Society (CUEiMS)
- The Trinity Mathematical Society
- Wednesday Seminars at the Computer Laboratory
- ResearchGate
- The Mathematics Genealogy Project
- Postdocs of Cambridge Society
- Machine Intelligence Research Institute