To Whom It May Concern,

I am a mathematician and programmer, who moved to Germany several years ago.

For many years i studied studied foundations of mathematics and proof assistants (HOL4, Coq, Isabelle, Metamath).

Currently I am writing a book about foundations of mathematics. (~90pages now)

My activities/achievements related to foundations of mathematics:

1) formulated super-small presentation of foundations of mathematics via Morse-Kelley class theory, for implementing in my proof assistant.

2) As a hobby, I have implemented my LCF proof assistant with tactics, etc. (1st order logic, classtheory Morse-Kelley).

Currently, playing Isabelle's metatheory, for formally proving soundness of higher-order statements of Isabelle, including those about the first order logic.

3) invented some really nice class-theoretic notions and proved theorems about them. (unpublished, but **very reliable**, some constructions and theorems are formally verified in The Coq Proof Assistant)

4) invented new semantics for certain extension of the 1st order logic, natural & useful: it has nice properties for working with "greek-letter-operators", and nicely treats different flavors of choice. Proved all necessary lemmas and theorems for its soundness. (unpublished, but **very reliable**)

5) have an idea of a new "natural" semantics for a metatheory of Isabelle. (just experimenting: It seems to be a bit exotic, but ok.)

**My goal is to work in TUM(or in other legal entity in Germany) on any project related to Isabelle or to foundations of mathematics and/or verification in general.**

I'd like and I have ability either to participate in existing Isabelle's project, or to do solo projects, and I can propose severak directions of work.

I am very open to new ideas/advises. Let's talk about it!

Kind regards,

Georgy Dunaev.

Last updated: Nov 11 2024 at 01:24 UTC