Keith J. Bauer

Stream: new members

[Keith J. Bauer]

The description of this area says to introduce oneself with a thread that has my name as the topic name. I am very new to Zulip, so I am not sure, but I don't see this type of thread at all when scrolling through the threads in "new members". Is this still correct to do?

[Scott Carnahan]

It is fine. Can you tell us more about yourself?What sort of formalization questions interest you?

[Yaël Dillies]

Hey Keith! :wave:

[Rida Hamadani]

Hi Keith :octopus:

[Keith J. Bauer]

Scott Carnahan said:

It is fine. Can you tell us more about yourself?What sort of formalization questions interest you?

Hi Scott. I'm an undergraduate student at University of California, Irvine. I'm currently interested in contributing to Lean's database of theorems. I have yet to look too much into the process of contributing because I am still somewhat new to Lean; to practice, I have been coming up with small theorems to practice formalizing. (i.e. I have practiced using Lean by proving that every commutative monoid induces its divisibility preorder, or that lex order on N^N is a linear order, etc.; nothing new mathematically nor to Lean (I assume) but good practice nonetheless.)

I'm currently working with Professor Isaac Goldbring, who has written a book on ultrafilters, so one thing I am interested in is what has been done with ultrafilters in Lean so far. Based on skimming mathlib, it seems basic things like their uses in topology and Los theorem are implemented, but I'm not sure how to find a comprehensive list of what has been done and what would be desired. Something Goldbring suggested to me was to look into whether Feferman-Vaught, the generalization of Los to reduced products, has been formalized yet, or to look into results relating to Ramsey cardinals, although I forget the exact details of the latter.

Additionally, this may be too ambitious, but I'm interested in what continuous logic has been formalized. (Goldbring is also very invested in continuous logic.) I say it may be too ambitious because if nothing at all has been done in this area, then it may be a lot of work for me to have to contribute even the very basics of something like that. But I don't know what I don't know, which is why I write here, to learn what is reasonable to expect.

Anyway, I hope to become well-acquainted with the Lean community in the coming months. My ultimate goal is to satisfy a requirement for undergraduate research from my school's honor's program (where I would ultimately write up the results of my efforts after 6 months) but otherwise my goal is to have fun proving cool theorems in Lean and contribute something to the community.

[Keith J. Bauer]

Yaël Dillies said:

Hey Keith! :wave:

Hi Yaël, I recognize you from Discord. I recall you mentioned you'd be around if I needed help with Lean, so maybe I will reach out to you on Discord more in that regard.

[Keith J. Bauer]

Rida Hamadani said:

Hi Keith :octopus:

Hi Rida, you were the one who ultimately got me interested in Lean, I'm glad to see you here as well. :)

[Aaron Anderson]

Of the projects you've suggested, I think the Feferman-Vaught project is most likely to produce good results in the timeframe you have - I've said more about my recommendations for that on the thread for that topic.

[Aaron Anderson]

Another thing that you could consider, specifically using ultrafilters, is Arrow's theorem. Someone has formalized Arrow's theorem in Lean before: https://github.com/asouther4/lean-social-choice/ , but they didn't use ultrafilters.

[Keith J. Bauer]

I forgot to respond here, but I think I will ultimately pursue Feferman-Vaught. From what you've said, I do agree.

[Keith J. Bauer]

I appreciate your detailed feedback.