Terence Tao

One nice thing is that there are now lots of sources for mathematical enrichment outside the classroom.

So, in my day, there were already math competitions.

And, you know, there are also popular math books in the library.

But,

Now you have YouTube.

There are forums devoted to solving math puzzles.

And math shows up in other places.

For example, there are hobbyists who play poker for fun.

And they, for very specific reasons, are interested in very specific probability questions.

And there's a community of amateur probabilists in poker.

In chess, in baseball, I mean, there's math all over the place.

And I'm hoping actually with these new sort of tools for Lean and so forth, that actually we can incorporate the broader public into math research projects.

Like this is almost, it doesn't happen at all currently.

So in the sciences, there's some scope for citizen science, like astronomers, the amateurs who discover comets, and there's biologists, there are people who identify butterflies and so forth.

And there are a small number of activities where amateur mathematicians can discover new primes and so forth.

But previously, because we had to verify every single contribution, most mathematical research projects, it would not help to have...

input from the general public.

In fact, it would just be time-consuming because just error-checking and everything.

But one thing about these formalization projects is that they are bringing together more, bringing in more people.

So I'm sure there are high school students who've already contributed to some of these formalizing projects, who've contributed to MathLib.