### Summary

Name | Manuel EBERL [ˈmaːnu̯ɛl ˈʔeːbɐl]
(feel free to call me by first name) |

<firstname.lastname>@uibk.ac.at (German, English, Esperanto) | |

PGP Key | 12A14807.asc |

CV | [PDF] |

ORCID | 0000-0002-4263-6571 |

Scholarly profiles | Google Scholar, DBLP |

Office | 3M12 in the ICT building (2nd floor) |

Office hours | Wednesday 14:15–15:45 (during term time only) |

@pruvisto | |

Mastodon | @pruvisto@graz.social (German/English) @pruvisto@esperanto.masto.host (Esperanto) |

Erdős number | ≤ 4 |

### About me

Since September 2021, I am a Postdoc at the Computational Logic Group at the University of Innsbruck. Before that, I did my PhD at the Technical University of Munich. I am also an editor of the *Archive of Formal Proofs*.

I mainly work on the formalisation of pure mathematics in Isabelle/HOL. I believe that the formalisation of a significant portion of known mathematics is a feasible and worthwhile endeavour.

My current work is the formalisation of the (semi-)automatic solving and verification of certain classes of mathematical problems, particularly those of the asymptotics of real-valued functions.

### Mathematical Interests

With varying levels of proficiency:

- Complex analysis
- Discrete mathematics, complexity analysis, analytic combinatorics, analytic number theory
- Abstract algebra and category theory
- Social choice theory
- Decision procedures
- Programming languages, functional programming, type systems, and program verification

### Current Work

- Analysis of Randomised Algorithms and Data Structures
- Semi-Automatic Real Asymptotics in Isabelle/HOL
- Formalisation of Tom Apostol's Introduction to Analytic Number Theory
- Continued Fractions