A Personal Website

Preprint with Jamie Vicary, 2023.

We now have a wide range of proof assis­tants avail­able for com­po­si­tional rea­son­ing in monoidal or higher cat­e­gories which are free on some gen­er­at­ing sig­na­ture. How­ever, none of these allow us to rep­re­sent cat­e­gor­i­cal oper­a­tions such as prod­ucts, equal­iz­ers, and sim­i­lar log­i­cal tech­niques. Here we show how the foun­da­tional math­e­mat­i­cal for­mal­ism of one such proof assis­tant can be gen­er­al­ized, replac­ing the con­ven­tional notion of string dia­gram as a geo­met­ri­cal entity liv­ing inside an n-cube with a pose­tal vari­ant that allows exotic branch­ing struc­ture. We show that these gen­er­al­ized dia­grams have richer behav­iour with respect to cat­e­gor­i­cal lim­its, and give an algo­rithm for com­put­ing lim­its in this set­ting, with a view towards future appli­ca­tion in proof assis­tants.

Preprint with Tobias Hartung and Karl Jansen, 2022.

Lat­tice field the­ory is a very pow­er­ful tool to study Feyn­man’s path inte­gral non-per­tur­ba­tively. How­ever, it usu­ally requires Euclid­ean back­ground met­rics to be well-defined. On the other hand, a recently devel­oped reg­u­lar­iza­tion scheme based on Fourier inte­gral oper­a­tor zeta-func­tions can treat Feyn­man’s path inte­gral non-per­tu­ba­tively in Lorentz­ian back­ground met­rics. In this arti­cle, we for­mally zeta-reg­u­lar­ize lat­tice the­o­ries with Lorentz­ian back­grounds and iden­tify con­di­tions for the Fourier inte­gral oper­a­tor zeta-func­tion reg­u­lar­iza­tion to be applic­a­ble. Fur­ther­more, we show that the clas­si­cal limit of the zeta-reg­u­lar­ized the­ory is inde­pen­dent of the reg­u­lar­iza­tion. Finally, we con­sider the har­monic oscil­la­tor as an explicit exam­ple. We dis­cuss mul­ti­ple options for the reg­u­lar­iza­tion and ana­lyt­i­cally show that they all repro­duce the cor­rect ground state energy on the lat­tice and in the con­tin­uum limit. Addi­tion­ally, we solve the har­monic oscil­la­tor on the lat­tice in Minkowski back­ground numer­i­cally.

Proof assis­tant with Nathan Corbyn, Lukas Heidemann, Nick Hu, Calin Tataru and Jamie Vicary, 2022.

The homotopy.io proof assis­tant allows the con­struc­tion of com­pos­ite mor­phisms in a finitely-gen­er­ated semi­strict n-cat­e­gory, via a point-and-click user inter­face. Com­pos­ites are ren­dered as 2d and 3d geome­tries, and can be visu­alised in 4d as movies of 3d geome­tries. Beyond its fea­tures as a visual proof assis­tant, homotopy.io can also be used as an effec­tive tool to type­set string dia­grams: any 2d dia­gram con­structed in the proof assis­tant can be exported with ease into LaTeX/TikZ and SVG, with exper­i­men­tal sup­port for manim. The proof assis­tant is imple­mented in the Rust pro­gram­ming lan­guage, and com­piled to WebAssem­bly to run in the web browser.