Dr. Angeliki KoutsoukouArgyraki
Lecturer in Computer Science, Royal Holloway, University of London
Visiting Researcher, University of Cambridge
College Research Associate, Clare College Cambridge
Contact: ak2110[at]cam[dot]ac[dot]uk, angeliki.koutsoukouargyraki[at]rhul[dot]ac[dot]uk
I participated in the ERC Project ALEXANDRIA (1/10/201731/8/2023)
led by Professor Lawrence C. Paulson at Cambridge as a postdoctoral researcher (Senior Research Associate: 5/20228/2023, Research Associate: 10/20174/2022)
and a member of the Programming Languages, Semantics and Verification
( Automated Reasoning ,
Programming, Logic and Semantics) Research Group
at the Computer Laboratory, University of Cambridge.
I am now affiliated to the University of Cambridge as a Visiting Researcher at the Department of Computer Science and Technology and a College Research Associate at Clare College.
I am also a participant in the new research project HumanOriented Automatic Theorem Proving
led by Professor Timothy Gowers at the Department of Pure Mathematics and Mathematical Statistics, University of Cambridge.
I was previously (10/20169/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.
ORCID MathSciNet ResearchGate
Research Interests
Formalization of mathematical proofs with Isabelle
; Interactive theorem proving and verification; Mechanisation of mathematics;
Automatic proof discovery;
Intersection of logic and mathematics; (Applied) proof theory, in particular I have been working on proof mining (penandpaper extraction of computable bounds from mathematical proofs) applied to proofs in nonlinear analysis, differential equations and fixed point theory; Foundations of mathematics.
Studies
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).
Journal Publications
 Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL (with Chelsea Edmonds and Lawrence C. Paulson), Journal of Automated Reasoning, volume 67, Article number: 2 (2023). (Published Online 19 Dec. 2022).
 Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL (with Wenda Li and Lawrence C. Paulson), Experimental Mathematics, Special Issue on Interactive Theorem Proving in Mathematics Research,
Volume 31, 2022  Issue 2, pages 401412. (Published Online 21 Oct. 2021).
 Formalising Ordinal Partition Relations Using Isabelle/HOL (with Mirna Džamonja and Lawrence C. Paulson), Experimental Mathematics, Special Issue on Interactive Theorem Proving in Mathematics Research, Volume 31, 2022  Issue 2, pages 383400. (Published Online 11 Oct. 2021).
 Formalising mathematicsin praxis; A mathematician's first experiences with Isabelle/HOL and the why and how of getting started, Jahresbericht der Deutschen MathematikerVereinigung vol. 123, 326 (2021).
 New effective bounds for the approximate common fixed points and asymptotic regularity of nonexpansive semigroups, Journal of Logic and Analysis, vol. 10:7, 130 (2018).
 Effective rates of convergence for the resolvents of accretive operators, Numerical Functional Analysis and Optimization, vol. 38, issue 12, 16011613 (2017).
 Effective asymptotic regularity for oneparameter nonexpansive semigroups (with Ulrich Kohlenbach), J. Math. Anal. Appl., vol. 433(2), 18831903 (2016).
 Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators (with Ulrich Kohlenbach), J. Math. Anal. Appl., vol. 423 (2), 10891112 (2015).
Conference Publications
 A Formalisation of the BalogSzemerédiGowers Theorem in Isabelle/HOL (with Mantas Bakšys and Chelsea Edmonds). In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’23), January 16–17, 2023, Boston, MA, USA. ACM, New York, NY, USA, 14 pages.
 What Can Formal Systems Do For Mathematics? A Discussion Through The Lens Of Proof Assistants: Some Recent Advances.. Q & A with Jeremy Avigad, Jasmin Blanchette, Frédéric Blanqui, Kevin Buzzard, Johan
Commelin, Manuel Eberl, Timothy Gowers, Peter Koepke, Assia Mahboubi, Ursula Martin, Lawrence C. Paulson. Invited Contribution.
B. Löwe, D. Sarikaya (eds.), 60 Jahre DVMLG,
Vol. 48 of Tributes, College Publications, London, 2022.
 On preserving the computational content of mathematical proofs: toy examples for a formalising strategy (Invited contribution) In: De Mol L., Weiermann A., Manea F., FernándezDuque D. (eds) Connecting with Computability. CiE 2021. Lecture Notes in Computer Science, vol 12813. Springer, Cham (2021). https://doi.org/10.1007/9783030800499_26
Longer version here
On the Archive of Formal Proofs
 Polygonal Number Theorem (with Kevin Lee and Zhengkun Ye), Aug. 2023.
 Kneser's Theorem and the CauchyDavenport Theorem (with Mantas Bakšys), Nov. 2022.
 The BalogSzemerédiGowers Theorem (with Mantas Bakšys and Chelsea Edmonds), Nov. 2022.
 Khovanskii's Theorem (with Lawrence C. Paulson), Sept. 2022.
 The PlünneckeRuzsa Inequality (with Lawrence C. Paulson), May 2022.
 Roth's Theorem on Arithmetic Progressions (with Chelsea Edmonds and Lawrence C. Paulson), Dec. 2021.
 Szemerédi's Regularity Lemma (with Chelsea Edmonds and Lawrence C. Paulson), Nov. 2021.
 Amicable Numbers, Aug. 2020.
 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.
Abstracts in Conference Proceedings
 Formalisation of Additive Combinatorics in Isabelle/HOL, Dagstuhl proceedings of the 14th International Conference on Interactive Theorem Proving (ITP 2023), July 31August 4, 2023 in Bialystok, Poland. (Invited contribution).
 SErAPIS: A ConceptOriented Search Engine for the Isabelle
Libraries Based on Natural Language (with Yiannos Stathopoulos and Lawrence C. Paulson), informal proceedings of the Isabelle Workshop 2020
affiliated to IJCAR 2020, (in Virtual Space), June 30, 2020.
 Developing a ConceptOriented Search Engine for Isabelle Based on Natural Language : Technical Challenges (with Yiannos Stathopoulos and Lawrence C. Paulson), informal Proceedings of the 5th Conference on Artificial Intelligence and Theorem Proving (AITP 2020), Aussois, France, Mar. 2227, POSTPONED TO Sept. 1318, 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 1619, 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.1420, 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 1216, 2017 , (Alexandra Soskova, Antonis Kakas, and Nikolaos Papaspyrou eds.).
 New Applications of Proof Mining to Nonlinear Analysis (with Ulrich Kohlenbach) in : Piecha, Thomas; SchröderHeister, Peter: General Proof Theory. Celebrating 50 Years of Dag Prawitz's "Natural Deduction". Proceedings of the Conference held in Tübingen, 2729 Nov. 2015.
 Prooftheoretic 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), 1622 Nov. 2014, Report No. 52/2014.
SErAPIS:
Yiannos Stathopoulos and I created a conceptoriented search engine for the Isabelle Libraries and the Archive of Formal Proofs.
Please try it out here and give us your relevance feedback after reading the user guide.
Fun with Maths
Talks (upcoming and past)
 Invited (tutorial) speaker at the 14th Panhellenic Logic Symposium, Thessaloniki, Greece, July 15, 2024.
 Invited speaker at the London Mathematical Society Computer Science Colloquium 2023, De Morgan House, London, Dec. 1, 2023.
 Invited speaker at Interactions of Proof Assistants and Mathematics, International Summer School, Regensburg, Germany, Sept. 1829, 2023.
 Invited speaker at ITP 2023 (14th Conference on Interactive Theorem Proving), Bialystok, Poland, July 31  Aug. 4, 2023.
 Invited speaker at the Topos Institute Colloquium, Online (6/10/2022). SLIDES and VIDEO.
 (cancelled)Invited speaker at the Colloquium Logicum, Konstanz, Germany,
Sept. 2326, 2020 postponed to Sept. 2021 2022
 Invited speaker at Proofs, Arguments and Dialogues, Summer School, University of Tübingen, 812 Aug., 2022.
SLIDES
 Invited Speaker at Computability in Europe 2021, HaPoC Special Session, Ghent, Belgium/ in Virtual Space, July 59, 2021.
 Invited speaker at the Online Logic Seminar,(21/1/2021).
 Invited speaker at the Big Proof Workshop, Edinburgh, UK, May 2731, 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. 712, 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 speakerspecial session on proof theory North American Annual Meeting of the Association for Symbolic Logic, University of Western Illinois, Macomb, Illinois, USA, May 1619, 2018.
 "An invitation to proof mining: two applications in nonlinear operator theory"(18/8/2017), Logic Colloquium 2017, Stockholm, Sweden, Aug.1420, 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 2627, 2017.
 ''Proof mining: An ''effective'' program (even) for ineffective Mathematics'' (15/7/2017), 11th Panhellenic Logic Symposium, Delphi, Greece, July 1216, 2017.
 ''Automorphisms of the Calkin algebra under two different settheoretic 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 , RuhrUniversity Bochum, Germany, May 24, 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. 2729, 2015.
 ''Effective information for abstract Cauchy problems extracted via Proof Mining'' (8/10/2015), SPP 1506, IRTG 1529 and DFGJSPS Joint International Conference and Autumn School, Darmstadt, Germany, Oct. 58, 2015.
 ''Approximate common fixed points and rates of asymptotic regularity for oneparameter nonexpansive semigroups'' (20/7/2015), 11th International Conference on Fixed Point Theory and Applications, Istanbul, Turkey, July 2024, 2015.
 ''Approximate common fixed points and rates of asymptotic regularity for oneparameter 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 1115, 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. 26, 2015.
 ''ProofTheoretic 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. 1622, 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 2425, 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. 2628, 2014.
 ''Proof Theory and PDEs''(29/1/2014) ,IRTG 1529 Winter Seminar and Klausurtagung, Chalet Giersch, La Clusaz, France, Jan. 2731, 2014.
 "Automorphisms of the Calkin algebra under two different settheoretic hypotheses; An independence result" (21/6/2013), Logic Seminar, TU Darmstadt, Germany.
 "Automorphisms of the Calkin algebra under two different settheoretic 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.
Academic Service/Other activities
 Participating in running the Proofs and Programs Club at Royal Holloway, University of London, since 1/2024.
 Coorganiser and member of the Programme Committee of the joint WG4 & WG5 EuroProofNet workshops (Workshop on Natural Formal Mathematics and Workshop on Libraries of Formal Proofs and Natural Mathematical Language), 68 Sept. 2023, Cambridge, UK.
 Coorganisation of a seminar series Formalisation of mathematics with interactive theorem provers,
joint between the Department of Computer Science and Technology and the Faculty of Mathematics at Cambridge, since 1/2023.
 Leader of Working Group 4 (Libraries of Formal Proofs) of COST Action CA20111  European Research Network on Formal Proofs. since 11/2022.
 Management Committee representative for the UK for the COST Action CA20111  European Research Network on Formal Proofs.
 Reviewer for Mathematical Reviews (AMS) (review list here)
 Member of the Research Staff Forum at the Computer Laboratory, University of Cambridge (Autumn 2018Summer 2023).
 Member of the Program Committees of: Computability in Europe 2025, ITP 2024 (15th Conference on Interactive Theorem Proving),
Computability in Europe 2023, CICM 2023, CICM 2022, Certified Programs and Proofs 2021 .
 Member of the local organisers of the
25th Automated Reasoning Workshop (Cambridge 1213 Apr. 2018) and of the
organising committee of ''PhDs in Logic VIII'' (TU Darmstadt, 911 May 2016).
 Served as an interviewer for Mathematics interviews for Computer Science undergraduate applicants at Clare College Cambridge (December 2023, December 2021, December 2020).
 Research stay at Waseda University, Tokyo, Japan (1/9/201410/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 London Mathematical Society, The Association for Computing Machinery, the Proof Society, the Association for Symbolic Logic , the British Logic Colloquium , the DVMLG and The Trinity Mathematical Society.
 Doktorandentreff
Teaching
 At Royal Holloway, University of London:
 Module leader for the 2nd year undergraduate course "Symbolic Artificial Intelligence" (212 students, Spring term 2024).
 Tutorials (exercise classes) for:
 Machine Fundamentals (1st year undergraduate course, 15 students, Spring term 2024).
 Mathematical Structures (1st year undergraduate course, 15 students, Autumn term 2023).
 Overseeing the Final Year Projects of four students, and the Year In Industry project of one student.
 At the University of Cambridge:
 Hosted three Cambridge Mathematics students, Zhengkun (Chris) Ye, Kevin Lee, and Yaël Dillies, for 8week summer internships during the summer of 2023
with the support of the Cambridge Mathematics Placement programme , formalising additive number theory/ combinatorics in Isabelle/HOL and Lean. Their work resulted in this AFP entry and this Lean repository.
 Supervised the Part III (i.e. MPhil) Project in Advanced Computer Science of Ryan Shao: “Formalisation of an Upper Bound for the Easier Waring’s Problem in Isabelle”. Honours Pass with Distinction. (20222023).
 Supervised the Part II (i.e. 3rd year) Project of Jamie Chen: “Formalising the Wieferich–Kempner Theorem in Isabelle/HOL” (20222023).
 Hosted a Cambridge Mathematics student, Mantas Bakšys, for an 8week summer internship during the summer of 2022
with the support of the Cambridge Mathematics Placement programme , formalising additive combinatorics in Isabelle/HOL. Resulted in a paper accepted for publication in Certified Programs and Proofs (CPP) 2023 and the AFP entries
1 and 2.
 Cosupervised (with Prof. Lawrence Paulson) Nils Lauermann's MPhil Project: "A Formalisation of Turán’s Graph Theorem in Isabelle/HOL"
AFP entry (20212022).
 Supervisions (exercise classes) for:
 At TU Darmstadt, Department of Mathematics:
 SoSe 2017Teaching Assistant for Proof Theory
 WiSe 20162017Teaching Assistant for
 Complex Analysis
 Differential Equations
 At the University of Copenhagen, Department of Mathematical Sciences:
 Exercise classes for Mathematical Physics (20102011, 20112012)
 LaTeX (2011, 2012).
Events to attend/ recently attended
 Workshop: Libraries of Digital Math,
July 29 Aug. 2, 2024, Trimester Program: Prospects of formal mathematics, Hausdorff Research Institute for Mathematics, Bonn, Germany.
 14th Panhellenic Logic Symposium, Thessaloniki, Greece, July 15, 2024.
 Workshop: Formalization of Mathematics, June 17  21, 2024, Trimester Program: Prospects of formal mathematics, Hausdorff Research Institute for Mathematics, Bonn, Germany.
 AI @Royal Holloway, Royal Holloway, University of London, June 10, 2024.
 AI to Assist Mathematical Reasoning: Webinar Series,
National Academies of Sciences, Engineering, and Medicine, (Online), April 2325, 2024.
 Structure and Randomness  a celebration of the mathematics of Timothy Gowers, Isaac Newton Institute for Mathematical Sciences, Cambridge, UK, April 812, 2024.
 London Mathematical Society Computer Science Colloquium 2023 Verification: Theory and Practice, De Morgan House, London, UK, Dec. 1, 2023.
 London Mathematical Society Annual Meeting, Nov. 17, 2023, Mary Ward House, London, UK.
 Interactions of Proof Assistants and Mathematics, International Summer School, Regensburg, Germany, Sept. 1829, 2023 (online attendance).
 Joint WG4 & WG5 EuroProofNet workshops (Workshop on Natural Formal Mathematics and Workshop on Libraries of Formal Proofs and Natural Mathematical Language), 68 Sept. 2023, Cambridge, UK.
 ITP 2023 (14th Conference on Interactive Theorem Proving), Bialystok, Poland, July 31  Aug. 4, 2023.
 General Meeting of the London Mathematical Society and Hardy Lecture 2023,
Mary Ward House, London, June 30, 2023.
 AI to Assist Mathematical Reasoning: A Workshop (Virtual),
National Academies of Sciences, Engineering, and Medicine, June 1214, 2023.
 New Perspectives in Pure Mathematics, Heilbronn Institute for Mathematical Research,
University of Bristol, Mar. 2729, 2023.

Machine Assisted Proofs, IPAM, UCLA (online), Feb. 1317, 2023.
 Computer Guided Mathematics Symposium (GResearch Distinguished Speaker Series) , London, Nov. 22, 2022.
 EuroProofNet Workshop on the development, maintenance, refactoring and search of large libraries of proofs, (Online), Sept. 2324, 2022.
 15th Conference on Intelligent Computer Mathematics (CICM 2022), (Tbilisi, Georgia/in Virtual Space), Sept. 1923, 2022.
 Isabelle Workshop 2022, (Online), Aug. 11 2022.
 Proofs, Arguments and Dialogues, Summer School, University of Tübingen (Online), Aug. 812, 2022.
 Mathematical Theorem Proving Workshop, HUAWEI, Cambridge, April 25, 2022.
 MachineChecked MathematicsA meeting for mathematical formalizers
, Lorentz Center, Universiteit Leiden, Online, Mar. 24, 2022.

Formalize!(?)2, Zurich / Online, Jan. 15, 2022.
 The Meaning of Proofs: Celebrating the World Logic Day 2022 , University College London/ Online, Jan. 14, 2022.
 Autumn school "Proof and Computation", in Virtual Space, Sept. 1314, 2021.
 6th Conference on Artificial Intelligence and Theorem Proving (AITP 2021), in Virtual Space/Aussois, France, Sept. 511, 2021.
 TextDriven Approaches to the Philosophy of Mathematics 2 (in Virtual Space), Universität Duisburg Essen, Sept 13, 2021.
 14th Conference on Intelligent Computer Mathematics (CICM 2021), Timisoara, Romania (in Virtual Space), July 2631, 2021.
 Computability in Europe 2021, Ghent, Belgium/ in Virtual Space, July 59, 2021.
 ICLR21 Workshop on Responsible AI, in Virtual Space, May 7, 2021.
 ICLR21, MATHAI, The Role of Mathematical Reasoning in General Artificial Intelligence, in Virtual Space, May 7, 2021.
 When deep learning meets logic, in Virtual Space, Feb. 1517, 2021.
 Formalize!(?), Zurich/in Virtual Space, Jan. 16, 2021.
 London Mathematical Society Computer Science Colloquium, London, UK (in Virtual Space), Nov. 19, 2020.
 Logical Perspectives Open Lectures 2020,(in Virtual Space), Nov. 1718, 2020.
 5th Conference on Artificial Intelligence and Theorem Proving (AITP 2020), Aussois, France,
Mar. 2227 postponed to Sept. 1318, 2020.
 13th Conference on Intelligent Computer Mathematics (CICM 2020), (in Virtual Space), July 2730, 2020.
 Isabelle Workshop 2020,(in Virtual Space), June 30, 2020.
 IJCAR 2020,(in Virtual Space), June 29July 6, 2020.
 The Big Mathematics Initiative, ICMS Edinburgh (in Virtual Space), June 11, 2020.
 2nd Logipedia Meeting, ENSParisSaclay, Paris, France, Jan. 2728, 2020.
 Tableaux 2019/ 26th Automated Reasoning Workshop(ARW 2019), London, UK, Sept. 23, 2019.
 Big Proof Workshop, Edinburgh, UK, May 2731, 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. 712, 2019.
 The Second Meeting in Ethics in Mathematics (EiM2), Cambridge, UK, Apr. 35, 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. 1920, 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 912, 2018.
 Workshop on Proof Complexity (PC 2018), Oxford, UK, July 78, 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 1619, 2018.
 25th Automated Reasoning Workshop (ARW 2018), Cambridge, UK, Apr. 1213, 2018.
 Foundations in Mathematics: Modern Views, Munich, Germany, Apr. 47, 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. 1517, 2017.
 Autumn school "Proof and Computation", Herrsching, Germany, Sept. 2326, 2017.
 Logic Colloquium 2017, Stockholm, Sweden, Aug.1420, 2017.
 Proof, Computation, Complexity 2017 Sixteenth International Workshop, Göttingen, Germany, July 2627, 2017.
 11th Panhellenic Logic Symposium, Delphi, Greece, July 1216, 2017.
 Computeraided mathematical proof , Isaac Newton Institute for Mathematical Sciences, Cambridge, UK, July 1014, 2017.
 PhDs in Logic IX , RuhrUniversity Bochum, Germany, May 24, 2017.
 Colloquium Logicum 2016, Hamburg, Germany, Sept. 1012, 2016.
 World Congress in Philosophy 2016 , Athens, Greece, July 915, 2016.
 PhDs in Logic VIII , TU Darmstadt, Germany, May 911, 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. 2729, 2015.
 SPP 1506, IRTG 1529 and DFGJSPS Joint International Conference and Autumn School, Darmstadt, Germany, Oct. 58, 2015.
 11th International Conference on Fixed Point Theory and Applications, Istanbul, Turkey, July 2024, 2015.
 Tenth International Conference on Computability, Complexity and Randomness, Heidelberg, Germany, June 2226, 2015.
 10th Panhellenic Logic Symposium , Samos, Greece, June 1115, 2015.
 PhDs in Logic VII, Vienna, Austria, May 1416, 2015.
 JSPSNUS Joint Workshop in Mathematical Logic and Foundations of Mathematics, Kanazawa, Japan, Mar. 68, 2015.
 Constructivism and Computability, JAIST Logic Workshop Series, Kanazawa, Japan, Mar. 26, 2015.
 RIMS Workshop on Proof Theory, Computation Theory and Related Topics , Kyoto, Japan, Dec. 2426, 2014.
 Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics, Mathematical Research Institute Oberwolfach, Nov. 1622, 2014.
 Eleventh International Conference on Computability and Complexity in Analysis, TU Darmstadt, Germany, July 2124, 2014.
 PhDs in Logic VI, Utrecht, the Netherlands, April 2425, 2014.
 IRTG 1529 Research Seminar "Proof Mining and Nonlinear Analysis", TU Darmstadt, Germany, Feb. 2628, 2014.
 IRTG 1529 Winter Seminar and Klausurtagung, Chalet Giersch, La Clusaz, France, Jan. 2731, 2014.
 9th Panhellenic Logic Symposium , Athens, Greece, July 1518, 2013.
 6th Young Set Theory Workshop, Santuario di Oropa, Italy, June 1014, 2013.
 Workshop on Modal Logic: Modality and Modalities, Roskilde University, Denmark, May 2324, 2013.
 Workshop on Intensionality in Mathematics, Filosofiska Institutionen, Lund, Sweden, May 1112, 2013.
 Workshop on Applications to Operator Algebras, The Fields Institute for Research in Mathematical Sciences, Toronto, Canada, Sept. 1014, 2012.
 Appalachian Set Theory Workshop on C* algebras, Classification and Descriptive Set Theory, The Fields Institute for Research in Mathematical Sciences, Toronto, Canada, Sept. 89, 2012.
 8th Scandinavian Logic Symposium, Roskilde University, Denmark, Aug. 2021, 2012.
 Asian Initiative for Infinity (AII) Graduate Summer School, Institute for Mathematical Sciences (IMS), National University of Singapore, June 20July 17, 2012.
Favourite Links