Dr. Angeliki Koutsoukou-Argyraki

      

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

UPDATE: I recently (1/9/2023) joined Royal Holloway, University of London as a Lecturer in Computer Science.

My NEW WEBPAGE is in progress.

   

I participated in the ERC Project ALEXANDRIA (1/10/2017-31/8/2023) led by Professor Lawrence C. Paulson at Cambridge as a postdoctoral researcher (Senior Research Associate: 5/2022-8/2023, Research Associate: 10/2017-4/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 Human-Oriented Automatic Theorem Proving led by Professor Timothy Gowers at the Department of Pure Mathematics and Mathematical Statistics, University of Cambridge.

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.

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

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 401-412. (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 383-400. (Published Online 11 Oct. 2021).
• Formalising mathematics-in praxis; A mathematician's first experiences with Isabelle/HOL and the why and how of getting started, Jahresbericht der Deutschen Mathematiker-Vereinigung vol. 123, 3-26 (2021).
• New effective bounds for the approximate common fixed points and asymptotic regularity of nonexpansive semigroups, Journal of Logic and Analysis, vol. 10:7, 1-30 (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(2), 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 (2), 1089-1112 (2015).

Conference Publications

• A Formalisation of the Balog-Szemerédi-Gowers 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ández-Duque D. (eds) Connecting with Computability. CiE 2021. Lecture Notes in Computer Science, vol 12813. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-80049-9_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 Cauchy-Davenport Theorem (with Mantas Bakšys), Nov. 2022.
• The Balog-Szemerédi-Gowers Theorem (with Mantas Bakšys and Chelsea Edmonds), Nov. 2022.
• Khovanskii's Theorem (with Lawrence C. Paulson), Sept. 2022.
• The Plünnecke-Ruzsa 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 31-August 4, 2023 in Bialystok, Poland. (Invited contribution).
• SErAPIS: A Concept-Oriented 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 Concept-Oriented 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. 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.

SErAPIS: Yiannos Stathopoulos and I created a concept-oriented 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

• Geometrie auf der Straße, Geometrie für Alle (in German), Mitteilungen der Deutschen Mathematiker-Vereinigung, 29:4 (2021).

Talks (upcoming and past)

• Invited (tutorial) speaker at the 14th Panhellenic Logic Symposium, Thessaloniki, Greece, July 1-5, 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. 18-29, 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. 23-26, 2020 postponed to Sept. 2021 2022
• Invited speaker at Proofs, Arguments and Dialogues, Summer School, University of Tübingen, 8-12 Aug., 2022. SLIDES
• Invited Speaker at Computability in Europe 2021, HaPoC Special Session, Ghent, Belgium/ in Virtual Space, July 5-9, 2021.
• Invited speaker at the Online Logic Seminar,(21/1/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.

Academic Service/Other activities

• Participating in running the Proofs and Programs Club at Royal Holloway, University of London, since 1/2024.
• Co-organiser 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), 6-8 Sept. 2023, Cambridge, UK.
• Organisation 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 2018-Summer 2023).
• Member of the Program Committees of: 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 12-13 Apr. 2018) and of the organising committee of ''PhDs in Logic VIII'' (TU Darmstadt, 9-11 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/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 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 8-week 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. (2022-2023).
  • Supervised the Part II (i.e. 3rd year) Project of Jamie Chen: “Formalising the Wieferich–Kempner Theorem in Isabelle/HOL” (2022-2023).
  • Hosted a Cambridge Mathematics student, Mantas Bakšys, for an 8-week 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.
  • Co-supervised (with Prof. Lawrence Paulson) Nils Lauermann's MPhil Project: "A Formalisation of Turán’s Graph Theorem in Isabelle/HOL" AFP entry (2021-2022).
  • Supervisions (exercise classes) for:
    • Discrete Mathematics (Michaelmas Term 2021-Lent Term 2022), (Michaelmas Term 2020-Lent Term 2021).
    • Logic and Proof (Lent Term 2023), (Lent Term 2022), (Lent Term 2021), (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
    • Differential Equations
• At the University of Copenhagen, Department of Mathematical Sciences:
  • Exercise classes for Mathematical Physics (2010-2011, 2011-2012)
  • LaTeX (2011, 2012).

Events to attend/ recently attended

• Trimester Program: "Prospects of formal mathematics", Hausdorff Research Institute for Mathematics, Bonn, Germany.
• 14th Panhellenic Logic Symposium, Thessaloniki, Greece, July 1-5, 2024.
• AI to Assist Mathematical Reasoning: Webinar Series, National Academies of Sciences, Engineering, and Medicine, (Online), April 23-25, 2024.
• Structure and Randomness - a celebration of the mathematics of Timothy Gowers, Isaac Newton Institute for Mathematical Sciences, Cambridge, UK, April 8-12, 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. 18-29, 2023 (online attendance).
• Joint WG4 & WG5 EuroProofNet workshops (Workshop on Natural Formal Mathematics and Workshop on Libraries of Formal Proofs and Natural Mathematical Language), 6-8 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 12-14, 2023.
• New Perspectives in Pure Mathematics, Heilbronn Institute for Mathematical Research, University of Bristol, Mar. 27-29, 2023.
• Machine Assisted Proofs, IPAM, UCLA (online), Feb. 13-17, 2023.
• Computer Guided Mathematics Symposium (G-Research Distinguished Speaker Series) , London, Nov. 22, 2022.
• EuroProofNet Workshop on the development, maintenance, refactoring and search of large libraries of proofs, (Online), Sept. 23-24, 2022.
• 15th Conference on Intelligent Computer Mathematics (CICM 2022), (Tbilisi, Georgia/in Virtual Space), Sept. 19-23, 2022.
• Isabelle Workshop 2022, (Online), Aug. 11 2022.
• Proofs, Arguments and Dialogues, Summer School, University of Tübingen (Online), Aug. 8-12, 2022.
• Mathematical Theorem Proving Workshop, HUAWEI, Cambridge, April 25, 2022.
• Machine-Checked Mathematics-A meeting for mathematical formalizers , Lorentz Center, Universiteit Leiden, Online, Mar. 2-4, 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. 13-14, 2021.
• 6th Conference on Artificial Intelligence and Theorem Proving (AITP 2021), in Virtual Space/Aussois, France, Sept. 5-11, 2021.
• Text-Driven Approaches to the Philosophy of Mathematics 2 (in Virtual Space), Universität Duisburg Essen, Sept 1-3, 2021.
• 14th Conference on Intelligent Computer Mathematics (CICM 2021), Timisoara, Romania (in Virtual Space), July 26-31, 2021.
• Computability in Europe 2021, Ghent, Belgium/ in Virtual Space, July 5-9, 2021.
• ICLR-21 Workshop on Responsible AI, in Virtual Space, May 7, 2021.
• ICLR-21, MATH-AI, The Role of Mathematical Reasoning in General Artificial Intelligence, in Virtual Space, May 7, 2021.
• When deep learning meets logic, in Virtual Space, Feb. 15-17, 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. 17-18, 2020.
• 5th Conference on Artificial Intelligence and Theorem Proving (AITP 2020), Aussois, France, Mar. 22-27 postponed to Sept. 13-18, 2020.
• 13th Conference on Intelligent Computer Mathematics (CICM 2020), (in Virtual Space), July 27-30, 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.
• 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.

Favourite Links

• Seminar series: Formalisation of mathematics with interactive theorem provers
• Github
• Isabelle Zulip chat
• Lean Zulip chat
• The Number Theory Web Seminar
• The On-line Encyclopaedia of Integer Sequences
• Machine Logic (Blog by Lawrence C. Paulson)
• Terence Tao's Blog
• Timothy Gowers's Blog
• The Xena Project(Blog by Kevin Buzzard)
• Lean Community Blog
• Clare College, University of Cambridge
• 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