thomaskwaring.github.io/math.html at master · thomaskwaring/thomaskwaring.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
<!DOCTYPE html>
<html>
<head>
<title>Thomas Waring</title>
<!-- <link rel="stylesheet" type="text/css" href="/css/main.css"> -->
<link rel="stylesheet" href="main.css">
</head>


<body>
  <nav>
          <ul>
              <li><a href="https://thomaskwaring.github.io" class="nav-link">Home</a></li>
              <li><a href="https://thomaskwaring.github.io/cv.pdf" class="nav-link">CV</a></li>
        <li><a href="https://thomaskwaring.github.io/math.html" class="nav-link">Mathematics</a></li>
          </ul>
      </nav>

<h1>Mathematics</h1>
<p>
  I will collect here my notes & links to any talks that I give. Please let me know if anything is incorrect or unclear, or if you have any questions!
</p>

<ul>
  <li>My <a href="https://thomaskwaring.github.io/thesis.pdf">MSc thesis</a>, on <em>Geometric Perspectives on Program Synthesis and Semantics</em> (October 2021). Abstract:
    <blockquote>
      We develop a formalism to apply Watanabe’s Singular Learning Theory to the problem of program synthesis. In our case, a program is a sequence of letters on the tape of a Turing Machine, which we associate to a singularity of an analytic function. The key invariant associated to a singularity in this context is the real log canonical threshold, and we introduce methods to compute this value from an ideal generated by polynomials. We provide a semantic interpretation of these singularities, which distinguishes distinct algorithms by viewing them as the limit of a learning process.
    </blockquote>
  Some addenda:
  <ul>
    <li>An <a href="https://thomaskwaring.github.io/rlcts.pdf">informal appendix</a>, on blowing-up and calculating RLCTs.</li>

    <li> A talk on <em>regularly parametrised models</em>, to the <a href="https://metauni.org/posts/events/seminar-slt">Singular Learning Theory seminar</a> at metauni: <a href="https://thomaskwaring.github.io/reg-talk.pdf">notes</a> (March 2022).
    </li>
  </ul>
  </li>

  <li>A talk, given to a general audience, giving a brief history of the connection between proof theory and computation: <a href="https://thomaskwaring.github.io/proofs-computation-notes.pdf">notes</a>, and <a href="https://thomaskwaring.github.io/proofs-computation-slides.pdf">slides</a>. Given at il Collegio Universitario "Lamaro Pozziani" (February 2025).</li>

  <li>I have been learning the <a href="https://lean-lang.org/">Lean proof assistant</a>. Recently, I contributed a <a href="https://github.com/leanprover/cslib/tree/main/Cslib/Languages/CombinatoryLogic">formalisation of Combinatory Logic</a> to a project developing a general-purpose computer-science library.</li>

  <li><a href="https://thomaskwaring.github.io/f-norm.pdf">Notes</a> on Girard's strong normalisation theorem for System F (polymorphic lambda-calculus). Also includes some discussion of the relationship to Gödel's incompleteness theorems and second-order Peano arithmetic, expanding on some fairly cryptic remarks in Proofs and Types. (September 2020.) I gave a talk to the <a href="https://cglseminar.github.io/">Computation, Geometry, Logic</a> seminar based on these notes (July 2021, video lost to lockdown restrictions).</li>

  <li> A <a href="https://thomaskwaring.github.io/adsn_poster.pdf">poster</a> and <a href="https://doi.org/10.1111/2041-210X.14374">paper</a>, on a partially observed model of invasive species control, published by <em>Methods in Ecology and Evolution</em>. Work conducted at the Melbourne Centre for Data Science. (July 2023, <a href="https://thomaskwaring.github.io/pomdp_supp.html">supplementary material</a>.) </li>

  <li> <a href="https://thomaskwaring.github.io/young.pdf">A short note</a> on lattice paths in Young diagrams. I provide a (seemingly novel) bijective proof of an identity due to Carlitz, Roselle & Scoville, and answer explicitly an unsolved question raised in Stanley's Enumerative Combinatorics.</li>

  <li>For practice and my own benefit, I am working on translating some papers from French, which I will collect here.
    <ul class="inner-space">
      <li>JP Serre's <a href="https://thomaskwaring.github.io/gaga.pdf"><em>Géométrie algébrique et géométrie analytique</em></a> (GAGA, to his friends). I have, currently at least, skipped some of the applications for which I didn't have the necessary background. (November 2021.)</li>
      <li>"Inside every proof theorist is a sleeping bureaucrat." Jean-Yves Girard's <a href="https://thomaskwaring.github.io/proofs.pdf">From why to how: proof theory since 1950</a>. Come for the insights, stay for the snarky footnotes. (December 2021.)</li>
    </ul>
  </li>

</ul>

<footer>
  <a href="mailto:thomas.waring99@gmail.com" class="nav-link">email me</a>
</footer>

</body>
</html>