Aaron Liu (self-introduction)

Stream: new members

[Aaron Liu]

@Patrick Massot suggested I introduce myself.

Hi! I am Aaron Liu, a high schooler (grade 10) with too much free time. I've learnt most of my math from youtube, wikipedia, and google, just clicking on whatever looks interesting. I've been using Lean for about 8 months now.

I've worked through #nng, #tpil, and about half of Formalizing Mathematics. I practiced using Lean by proving some theorems not in mathlib.

[Kevin Buzzard]

Welcome along! Do you have a project you're working on, or are you content to just make many helpful comments?

[Aaron Liu]

I have some things that I work on occasionally in my free time. I've finished 6 of these small projects so far, including stuff like computable Real.sqrt, the Galois insertion from sets into sequentially closed sets (does this have a name?), and Niven's theorem (sin and cos version).

[Patrick Massot]

Nice! Where are you living?

[Aaron Liu]

I live near Pittsburgh, PA, USA

[Patrick Massot]

Oh, that’s a great answer. Have you visited the Hoskinson center already? I’m sure Jeremy and his gang would be happy to meet you.

[Jeremy Avigad]

@Aaron Liu You can visit us at Carnegie Mellon any time! We have a weekly Hoskinson Center meeting on Wednesdays at 4:30, which is a good way to talk to people about what you and they are doing, but we can also make other arrangements.