Jörn Stöhler

Stream: new members

[Jörn Stöhler]

Hi everyone!
Just wanna introduce myself and why I'm interested in Lean.
I am a MSc math student at University Augsburg (Germany).
I'm new to Lean, but have had some exposure (~20h) to proof assistants & program verification in general before. I hope to use Lean in my master's thesis.

My thesis topic is in the area of symplectic geometry. Concretely: I use computational and data science methods to form conjectures about on what 4d polytopes Viterbo's conjecture is true and false. There's been a recent simple counterexample (https://arxiv.org/abs/2405.16513 ) after 20y, which inspired this thesis topic.

Right now I'm looking into how to use Lean to work faster when ensuring that my algorithms are reliable. They've grown in complexity over the last 4 weeks and I spend more time on finding and fixing bugs and logical errors than I'd like. I've long used AI assistants in my work (GPT-5 atm via Codex CLI), for both software development and mathematical reasoning.

The "plan" is to use AI to accelerate the synchronization between

1. high-level research project management
2. human-written sketches of research questions, proofs, algorithms
3. detailed elaboration and specifications that resolve low-level questions
4. formalization of conjectures, theorems and proofs (using Lean)
5. high performance computing in (mixed) Rust/Torch/Python/C++

I generally had good experiences so far on the software engineering side with using AI assistants for 2<->3<->5 workflows. Since GPT-5 I also use them on the math side. The correspondence 3->5 between a detailed algorithm specification to AI-written code is quite robust and nearly a free action.

Concretely, GPT-5 and I right now struggle to implement an actually correct algorithm to check Viterbo's conjecture on a given polytope, because it's easy to overlook/gloss over when a lemma isn't stated in a form that's actually true for all relevant cases (for all relevant polytopes), or that an algorithm step does not actually fulfill the requirements of the lemmas we'd like. My guess is that I'd work faster if I got a better fast signal for when the specification of an algorithm isn't sound. Switching from Python to Rust's type system was already useful in a bunch of places here, as GPT-5 works slightly more autonomously in Rust than in Python and could identify bugs/errors in the specification more often.

My guess therefore is that letting GPT-5 formalize the algorithms in Lean will provide an additional valuable signal, more so than if the formalization happened just on paper without proof assistance + formal verification.
The correspondence of Lean to Rust code seems again like a free action, for the same reasons that the correspondence from detailed specifications to Rust code so far was robustly handled by GPT-5.

Besides working on my thesis, I maintain an active interest and background in other areas of pure math, computational physics, deep learning, technical ASI alignment, anti-ASI governance, and applications of AGI assistants (e.g. in my thesis as mentioned above).

Thanks to the Lean community by the way for all the great resources when learning Lean! Not sure who precisely has been impactful here, but it is a joy to read the docs, read example code, and use Lean in vscode.