Georgy Dunaev (Jul 09 2024 at 18:52): Georgy Dunaev (Jul 09 2024 at 18:52):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: Dec 03 2024 at 16:25 UTC