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).

- 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.

- Developing a Concept-Oriented Search Engine for Isabelle Based on Natural Language : Technical Challenges (with Yiannos Stathopoulos and Lawrence Paulson), to appear in the Proceedings of the 5th Conference on Artificial Intelligence and Theorem Proving (AITP 2020), Aussois, France, Mar. 22-27, 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.
- 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.

- 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

- Supervision for Logic and Proof (Lent Term 2020).

*At the University of Cambridge:*Supervision for Logic and Proof (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.
- 5th Conference on Artificial Intelligence and Theorem Proving (AITP 2020), Aussois, France, Mar. 22-27, 2020.
- 7th Oxbridge Women in Computer Science Conference, Cambridge, UK, Mar. 12
- 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
- MathOverflow
- 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