Weekly Topic (or maybe The Lean Theorem Prover discussion)

This is our main weekly meet where we discuss whatever math topic (or topics) have captured our attention of late. To give an idea, some past topics have centered around graph isomorphism, math programming (both practical and theoretical issues such as "how to use LaTex" or The Halting Problem), unsolved problems and riddles such as the Travelling Salesman Problem or P vs. NP, or learning interesting areas of math that are already known such as how to generate the Mandelbrot Set or how to use Cantor diagonalization to prove the existence of uncountable infinities.

Although people are welcome to bring a formal presentation on their topic of choice, this is by no means required nor even common. Most often we show up and ask each other what we've been working on lately; whatever seems to garner the most interest from the entire group is then what we discuss for the next fifty-odd minutes.

FAQ: Why "or maybe The Lean Theorem Prover discussion" ?

A: Lean is a powerful theorem prover. People in Lean community seem to be trying to formalize all mathematics and have gone pretty far in this effort.
https://leanprover.github.io/theorem_proving_in_lean/index.html
https://leanprover-community.github.io/100.html
https://github.com/leanprover-community/mathlib/tree/master/src

All mathematics is built on theorems and their proofs. At the same time, it might be very hard to navigate to a particular topic(theorem) of interest and abstract from everything else it depends on (this technique is very useful in programming). Especially if you're not a professional. Lean seems to be able to solve this problem, so everybody can jump right in the middle of a math course and still be able to grasp the idea with a reasonable amount of effort (instead of starting form scratch/basics).

If you are new to the group, or if you've never attended one of our meets before, go ahead and read the additional info below. Thanks!

𝛼 β 𝛾 Δ 𝜀 𝜁 η 𝜽 𝜄 𝜅 ƛ μ ν ξ ο π 𝜌 𝜎 𝜏 𝜐 𝜑 χ ѱ 𝛺
Welcome fellow numberphiles! Here is what you can expect at our next event:

Where ≈ Online - using Google Meet.

⨁ What we do = "Math for Fun" aims to be a group that is intellectually stimulating, yet accessible to anyone with a basic understanding of arithmetic and algebra.

⨁ Math for Fun is a zero stress group. Nothing is expected of anyone :-) If something sounds fun, go for it. Last minute change of plans? No worries. So have fun, don't stress, and hopefully drop in when it tickles your fancy!

In addition to our weekly video meets, our co-organizer Tyler has created an instant chat site as well as a weekly forum for this group. Here are the links:

⨁ Chat ⊨ https://chat.mathlink.org/math/channels/meetup
Optional app: https://mattermost.com/download/
This one is for instantaneous chat, usually used side-by-side with Zoom, good for typing up "math format" things. It supports LaTeX, but not math mode. For a new account link, message Tyler. Unfortunately, Mattermost doesn't seem to allow pending approval accounts. ∴

⨁ Forum ⊨ https://mathlink.org/
This one is a set of forums for more long-term topics/questions/discussions. Feel free to check and/or post here anytime between official meets. You can make an account, and I'll approve you soon after. If you don't get approved within a day, message me (Tyler). ∴

⨁ Cost = $0. There are no membership fees, attendance fees, nothing. This group is completely free. :) ∴

⋙ ⋙ ⋙ One last thing, and it's important: "Math for Fun" aims to be a fun and SAFE space for all. ⋘ ⋘ ⋘

We believe that diversity of human beings enhances diversity of ideas, and that respect for others leads to personal growth and vibrant communities. We would like to explicitly state that ALL cultures, colors, creeds, nationalities, orientations, genders, gender IDs, ages, economic levels, physical/cognitive abilities, and neurotypes, will not only be safe here but will be joyfully welcomed to participate. (Basically just pretend we live in Star Trek and you'll be doing it right. :P) Thanks for taking the time to read this, and for being courteous, compassionate, and curious human beings! ∴

See you there!

∑ Sam, Keith, Tyler, Nick