Bonn, DE

Stream: Geographic locality

[Anton Lorenzen]

Peter Koepke, Adrian De Lon and myself are here.

[Pit Sinning]

I currently study for my math b.sc in Bonn. I'm new to computational theorem proving/lean, but find the whole idea very intriguing.

[Floris van Doorn]

I will move to Bonn and join the Mathematical Institute at the University of Bonn on a (5 year) W2 professorship, starting October 1st. I have just officially accepted the offer a few minutes ago.
The subject of the professorship is specifically on formal mathematics and computer-assisted theorem proving, and I will also immediately start teaching a course on the formalization of mathematics in Lean this fall.

[Floris van Doorn]

I will be able to hire a post-doc almost right away. If you are looking for a post-doc position starting anytime in 2024 (or earlier - though that may be difficult), are willing to move to Bonn, and have plenty of Lean experience, please send me a short message, so that I know you're interested. I will post a more official job advertisement at a later point.

[Kevin Buzzard]

I'm going to be in Bonn from 10th to 21st June; 10th to 14th I'm going to be running a fairly informal workshop whose topic will be how to get the people who show up for the first lecture to help me prove Fermat's Last Theorem.

[María Inés de Frutos Fernández]

I am in Bonn until the 7th of July.

[Dean Young]

As of today I will be in Bonn by the 10th

[Patrick Massot]

I just arrived in Bonn. I’ll stay for two weeks.

[Chris Birkbeck]

I have just arrived in Bonn and will be here until the 28th (June).

[Dean Young]

@Patrick Massot @María Inés de Frutos Fernández @Kevin Buzzard @Floris van Doorn @Chris Birkbeck

I'm going to attend this here:

Screenshot-2024-06-16-at-3.48.05PM.png

And also the other two from this:

prospectsOfFormalMaths_poster_2024.jpeg

It's too bad I missed the workshop here. Is there anywhere a writeup I can look at?

[Kevin Buzzard]

Take a look at what's been going on in the FLT repo :-)

[Dean Young]

Based on the topics and María's presentations here and here, maybe the group would be interested in the relationship between norms and categories of modules:

• The set of Berkovich norms Ber(A) of a k-algebra A has as a (sub)basis D(f)= {ν : A // ν(f) ∈ (a,b) } , which produces the coarsest topology such that d(f) : Ber(A) → ℝ₀ ∪ {∞} sending ν to ν(f) is continuous.
• The completion Â of an algebra A with respect to the supremum of all of its Berkovich norms has the same Berkovich spectrum as A (the global Berkovich completion).
• There is an analogue of Gel'fand duality for [0,∞]-quantales which requires no C-star condition.
• Berkovich norms on an algebra A correspond to monoid preserving left adjoints F : A-mod ⭢ {-∞} ∪ ℝ ∪ {∞} , where the latter has the monoidal operation where -∞+x -= -∞, ∞+x = ∞ for x ≠ -∞, and x + y is addition of real numbers for x, y with x , y≠ -∞,x,y ≠ ∞.
• Valuations correspond to monoid preserving left adjoints F : R-mod ⭢ {-∞} ∪ Λ ∪ {∞}.
• Frames and locales are related to sober topological spaces. All spectral spaces and Hausdorff spaces are sober.
• The ideal lattice of a ring forms a quantale
• Krull's principal ideal theorem can be demonstrated in a quantale
• It is always possible to take the Berkovich completion after the algebraic closure of a field, to the effect that one does not need to take the algebraic closure afterwards or the Berkovich completion before.

[Dean Young]

@Kevin Buzzard Thanks,

wait this one right?

https://github.com/leanprover-community/flt-regular

[Ruben Van de Velde]

No

[Ruben Van de Velde]

https://github.com/ImperialCollegeLondon/FLT

[Dean Young]

Collaborative Formalization in Analysis

[Floris van Doorn]

Yeah, that is a seminar I'm doing with some students here. The repo is here: https://github.com/fpvandoorn/BonnAnalysis/
But I've been focusing myself more on a different project: https://github.com/fpvandoorn/carleson I will be announcing that project more broadly within a week.

[Dean Young]

@Floris van Doorn this looks interesting. Is it ok if I sit in on a few of these?

[Sebastian Ullrich]

I just arrived in Bonn and will be staying for two weeks

[María Inés de Frutos Fernández]

I have joined the University of Bonn as a postdoc in @Floris van Doorn 's group.

[Michael Rothgang]

I have also moved to Bonn, and will be working as a postdoc with @Floris van Doorn.
I intend to work more on formalisation of analysis (e.g. elliptic operators, perhaps elliptic regularity estimates, contributing to the Carleson project) and a bit less on linters and differential geometry --- but if you have a linter or differential (or even symplectic) geometry PR, I'll still be happy to review.

[Sébastien Gouëzel]

There is a differential geometry PR for you at #17358 :-) -- and I'm really unhappy about it, so ideas of better proofs are welcome. I'm showing that that the canonical equiv between the tangent bundle to a product, and the product of the tangent bundles, is smooth. For one direction, I have a functorial proof, takes two lines. For the other direction, I don't have a good proof, so I have to unfold too much, and it takes 150 lines :-(