cl-informatik.uibk.ac.at Open in urlscan Pro
138.232.66.201  Public Scan

Submitted URL: http://pruvisto.org/
Effective URL: http://cl-informatik.uibk.ac.at/users/meberl//
Submission: On August 16 via manual from IN — Scanned from DE

Form analysis 0 forms found in the DOM

Text Content

Dr. rer. nat. Manuel Eberl   

Home Publications Formalisations Teaching Miscellanea
Main page
Summary About Me Mathematical Interests Current Work


SUMMARY



NameManuel EBERL  [ˈmaːnu̯ɛl ˈʔeːbɐl]
(feel free to call me by first name) Email<firstname.lastname>@uibk.ac.at
(German, English, Esperanto) PGP Key12A14807.asc CV[PDF]
ORCID0000-0002-4263-6571 Scholarly profilesGoogle Scholar, DBLP Office3M12 in
the ICT building (2nd floor) Office hoursWednesday 14:15–15:45 (during term time
only) Twitter@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