I am a PhD student in theoretical physics with Miranda Cheng and Christoph Weniger at the University of Amsterdam.
Note: automatically loaded from Inspire-HEP; entries will be missing if JavaScript is disabled.
Einstein's theory of special relativity replaced the Euclidean space at the heart of Galilean physics with the new geometry of Minkowski space. Aiming to establishing a verified foundation for special relativity, this MSc project continues the mechanization of an axiomatic system for Minkowski space developed by Schutz in the interactive theorem prover Isabelle/HOL. First, the existing partial formalization is critically reviewed and several changes made to it are discussed. A new mechanization of the third theorem of collinearity introduced in Schutz's monograph is discussed. This required the development of new rigorous proofs capturing geometric intuitions which Schutz apparently derives from pictorial representations. Techniques to avoid combinatorial explosions arising in the mechanization of geometric proofs, by capturing without loss of generality notions, are discussed.
No analytic expressions for the Ricci-flat metrics on compact Calabi-Yau manifolds are known, which has led to the development of multiple numerical approximation schemes. This thesis shows that a deep learning approach using the energy functionals introduced by Headrick and Nassar can replace existing methods to approximate Calabi-Yau metrics on projective varieties. Building on top of the algebraic metrics introduced for Donaldson's algorithm, the deep learning models introduced here can predict approximations to the Ricci-flat metric as a function of complex moduli parameters. A comparison with the benchmark of balanced metrics produced by Donaldson's algorithm indicates these approximations are of relatively higher accuracy, justifying it as an alternative, standalone approximation scheme. This approach is facilitated by modern machine learning frameworks, which provide efficient automatic differentiation that can be used to derive geometrical objects, and work with complicated, geometrically motivated loss functions.
The AWAKE experiment is designed to study electron acceleration in plasma wakefields driven by self-modulated proton bunches. This project focuses on analyzing the transverse, time-integrated profile of the proton bunches after selfmodulation in rubidium plasma. The size and shape of these profiles can be used to verify the presence of self-modulation for each event and to study the influence of experimental parameters on the modulation process.
The generation of phase space events in high energy particle physics is commonly done using a Metropolis-Hasting unweighting algorithm with fixed proposal distribution. The multi-channel Markov chain Monte Carlo algorithm (MC3) introduced in [1] proposes a mixing of the fixed proposal method with a local Metropolis update. Based on this framework, the feasibility and performance improvement of using Hamiltonian (Hybrid) Monte Carlo (HMC) is analyzed. Performance is measured based on the number of target density evaluations and the introduced autocorrelation between events. Based on the analysis of a toy problem, the combined HMC-MC3 is found to improve on the sample convergence behavior of the fixed target proposal and reduces the autocorrelation of the local HMC method for strongly peaked distributions. While the overall approach seems promising, various parameters must be tuned for individual target distributions to obtain optimal performance.