Jalex Stark (introduction)

Stream: new members

[Jalex Stark]

I've been here a while but still feel a little too anonymous; hopefully this will help.

I'll call myself a "rogue academic". A couple of years ago I was a grad student proving theorems about quantum computing. I left because academia is slow. Now I have a job that offers a particularly good package of pay + free time (especially in the WFH era), and I use that to work on Lean stuff. (and also some pure maths and some non-maths science) Despite working in industry, I'm not a very good software engineer :upside_down: (by the way if you are interested in a job or summer internship, I am excited to get you to interview with my employer)

I'm generally excited about creating / improving pipelines for young people to get into formalization. Codewars is in my opinion the most exciting thing that's happened here in the past couple of months. (though the improvement of the toolchains is a close second) @ROCKY KAMEN-RUBIO is on my payroll as a "student", and I have also made a positive number of private grants to people I've met on this server. I'm thinking about how to teach a class and/or advise some students this summer at Mathcamp (a camp for high schoolers with a competitive proof-based entrance exam) I'm involved with. (When I was a student at Mathcamp, @Julian Gilbey got me interested in LaTeX)

Over the next couple of years, I'm excited to formalize complexity theory in general (a la Arora and Barak) and MIP*=RE in particular. In the former, my current narrow goal is to prove lemmas about the is_O relation on runtimes of algorithms. In the latter, my current goal is to clarify the paper proof by characterizing some of its constructions as limits in an appropriate category.

[Johan Commelin]

Hey Jalex! Thanks for the introduction! I've seen a lot of posts by you here, but I still learnt something new (-;

[Patrick Massot]

For your online mathcamp, you should probably think about improving the natural number game. There is a lot of engineering work to do in this direction.

[Jalex Stark]

do we have a concrete list of issues? (maybe they're in the "lean game maker" github project?)

[Patrick Massot]

I remembered discussing stuff with Kevin, but this is probably not public. Let me search

[Patrick Massot]

I think the main issue is: because people kept asking questions, Kevin kept adding written explanations. As a result, the game now contains way too many sentences, especially for young people who want to do things or watch videos but not reading.

[Patrick Massot]

Two obvious fixes to try are: add video explanations or use something like http://ninodezign.com/25-free-jquery-plugins-for-doing-guided-tours-through-a-website/

[Patrick Massot]

If you have even more time then you can try to uncouple the game from the browser. It should be easier to write the game once and have people playing it either online or locally. A local version can have full Lean speed (by using a locally installed Lean, not compiled in WebAssembly) and either run in a browser or in a dedicated interface (for instance using my prototype Qt client).

[Jalex Stark]

Patrick Massot said:

I think the main issue is: because people kept asking questions, Kevin kept adding written explanations. As a result, the game now contains way too many sentences, especially for young people who want to do things or watch videos but not reading.

hmm interesting. I think this is not so much a problem with this specific audience (who are generally happy to read textbooks) but definitely seems worthwhile for the broader audience

[Patrick Massot]

Currently even if you have a full Lean toolchain installed you still can't enjoy both the interface and the local Lean speed

[Patrick Massot]

I think you are already too old to see the issue.

[Patrick Massot]

Kevin's son is definitely of mathcamp style, and he says he won't read that much

[Jalex Stark]

ah maybe I should spend more time watching young people play it for the first time

[Marc Huisinga]

Jalex Stark said:

Over the next couple of years, I'm excited to formalize complexity theory in general (a la Arora and Barak) and MIP*=RE in particular. In the former, my current narrow goal is to prove lemmas about the is_O relation on runtimes of algorithms. In the latter, my current goal is to clarify the paper proof by characterizing some of its constructions as limits in an appropriate category.

oh, that's cool! afaik there's very little formalized for CCT in general, despite it being an area of interest for computer scientists.

[Jalex Stark]

CCT?

[Marc Huisinga]

computational complexity theory, sorry.

[Jalex Stark]

hah, and the reason for that is that the "computer scientists" who do complexity and the "computer scientists" who do programming languages and development of interactive theorem provers are totally different people

[Marc Huisinga]

i've gotten so used to that acronym because it's the name of the arora and barak draft pdf :p

[Jalex Stark]

theory students largely think programming languages classes are just a hurdle to getting their PhD, and maybe also vice versa but I wouldn't know because I didn't tlak to any PL folks when I was in academia :P

[Marc Huisinga]

oh no, it isn't (anymore?). maybe i just renamed that file years ago and thought that it was the actual name? hmmm.

[Jalex Stark]

I think that Ryan O'Donnel claimed that the proo fo the time hierarchy theorem in Arora and Barak is wrong. I'm hopeful that a formal proof of that would convince some complexity folks to be interested

[Marc Huisinga]

oh, i spent a good deal of time thinking about that one for the exam. the general version, or the concrete one for n and n^1.5?

[Jalex Stark]

I'm also curious whether having formalized complexity theory makes studying CS theory more interesting to the kind of undergrad that writes a lot of haskell code

[Jalex Stark]

Yeah I think the claim was that for some tight exponent the proof was wrong and he wasn't even sure if the theorem was true up to that tightness

[Jalex Stark]

(I didn't learn basics from arora and barak, and in particular haven't read its proof(s) of the time hierarchy theorem)

[Marc Huisinga]

i think @Markus Himmel understands this stuff better than me. didn't you mention to me once that the general proofs are cleaner, or was that a different proof?

[Jalex Stark]

what is the "general" version of the theorem you're talking about?

[Jalex Stark]

Is it something like "if $t$ is a time-constructible function, then there are problems solvable in time $t$ but not in time $t^2$"?

I've seen people use latex, how does it work?

[Marc Huisinga]

the "draft" version of the book i have lying around only proves the theorem for O(n) and O(n^1.5) (which is also what we did in our CCT lecture):
image.png
then again, this draft is very old.

[Patrick Massot]

Use double dollars for inline math. I know :shrug:

[Patrick Massot]

And use ```latex for display math

[Mario Carneiro]

what does time constructible mean?

[Jalex Stark]

ah okay, thanks

[Jalex Stark]

it means something like "there is a Turing machine that on input $n$ prints $t(n)$ and whose runtime is $o(t(n))$"
morally, "without any asymptotic overhead, you can run a timer"

[Marc Huisinga]

image.png

[Marc Huisinga]

(here's the draft pdf: https://theory.cs.princeton.edu/complexity/book.pdf)

[ROCKY KAMEN-RUBIO]

Hi everyone!

I’m Rocky, Jalex’s “student” as they mentioned in their post. I’ve been posting some basic questions for the last few months (thank you all for your incredible support!). I did my undergrad in Physics/Applied Math, then moved to New York to try to become a professional dancer instead of going to grad school. Since my academic background wasn’t in pure math or functional programming, I’ve had a lot to learn and am still getting up to speed. Jalex asked me to think of myself in part as a beta-tester for the “on-boarding process”, so feel free to send me resources or problems if you want a noob to look at them. I’m also open to suggestions or comments for learning Lean myself.

If you’re also a Lean noob, feel free to reach out and we can be noobs together!

[Patrick Massot]

@ROCKY KAMEN-RUBIO did you try the new tutorials?

[Mathieu Guay-Paquet]

Jalex Stark said:

[...] I'll call myself a "rogue academic". [...]
[...] I'm thinking about how to teach a class and/or advise some students this summer at Mathcamp (a camp for high schoolers with a competitive proof-based entrance exam) I'm involved with. (When I was a student at Mathcamp, Julian Gilbey got me interested in LaTeX) [...]

From a fellow rogue academic and former Mathcamper (student and staff), hi! These introduction threads are great, I should probably write one too.

[ROCKY KAMEN-RUBIO]

Patrick Massot said:

ROCKY KAMEN-RUBIO did you try the new tutorials?

I'm working on them right now! I was actually struggling a bit with real numbers in Lean so this should be a valuable resource. I'll let you know once I'm done if I have any meaningful feedback.

[Reid Barton]

Hi Jalex, I just want to say that all of the projects you have in mind sound quite interesting, but I would be especially excited just to have any usable definition of the class P of polynomial-time algorithms ("usable" meaning, say, that one can reasonably easily prove that multiplication of natural numbers is in P when the inputs are encoded in binary). I think @Mario Carneiro may have had some ideas about how to do this at some point?

[Mario Carneiro]

Indeed, this conversation got me thinking about turing machines again, hence #2605

[Jalex Stark]

Yeah I have not yet equipped a notion of turing machine with a notion of runtime

[Jalex Stark]

I'm currently trying to get adept with using structures

[Jalex Stark]

last time i looked at turing machines in mathlib, there was a "register machine" style definition that was not terribly far to what CS theory people actually use. My current best guess is that i'll be writing code that compiles to that, but idk yet

[Mario Carneiro]

I want to extend the work in turing_machine.lean to prove that turing machines can simulate partial recursive functions, which will achieve @Reid Barton 's "usable P" I think

[Julian Gilbey]

Patrick Massot said:

I think the main issue is: because people kept asking questions, Kevin kept adding written explanations. As a result, the game now contains way too many sentences, especially for young people who want to do things or watch videos but not reading.

Hi Patrick,
Yes, that is indeed an issue. I was using it with some undergraduates, and there was just too much text for them. (Especially for one of my students who is dyslexic.)

[Julian Gilbey]

Jalex Stark said:

[...]
I'm generally excited about creating / improving pipelines for young people to get into formalization. Codewars is in my opinion the most exciting thing that's happened here in the past couple of months. (though the improvement of the toolchains is a close second) ROCKY KAMEN-RUBIO is on my payroll as a "student", and I have also made a positive number of private grants to people I've met on this server. I'm thinking about how to teach a class and/or advise some students this summer at Mathcamp (a camp for high schoolers with a competitive proof-based entrance exam) I'm involved with. (When I was a student at Mathcamp, Julian Gilbey got me interested in LaTeX)
[...]

Hi Jalex,

How lovely to hear from you! (And sorry for the very slow response - crazy times!)

This all sounds really interesting. I've found getting to grips with Lean quite tricky; there are lots of really niggly issues that make it hard. I had been trying (before I ran out of time) to code Atiyah & Macdonald's book "Introduction to Commutative Algebra" in Lean. With a lot of help, I managed after many hours to get Proposition 1.1 and Proposition 1.2 done, but it was surprisingly difficult for such elementary results. Even in tactic mode, there are many things which are mysterious to me!

Best wishes,

Julian

[Johan Commelin]

@Julian Gilbey You can get an exponential(?) speedup if you ask lots of questions here.

[Kevin Buzzard]

We now have new functionality in NNG -- we can fold stuff. There are currently 0 examples of this, but we've been experimenting on it in the real number game. This might be a really good way of cutting out a lot of the text, or at least putting it out of harm's way.