I asked Claude code to formalize with lean a proof for the knuth 3d hamiltonian cycles problem (odd cases for now) that also solved experimentally by claude - www-cs-faculty.stanford.edu/~knuth/paper...
github.com/rkirov/claud...
Read more in the human notes section in the README.
If they teach it directly with AI, they are not matching their own journey and might fail to translate the right lessons.
There is also a timing risk. The ai of tomorrow might not need steering. By the time you finish the course it might not be as needed.
Big +1, steering is mandatory today and it does involve at minimum reading the code. The main problem as I see it is everyone adept at steering has learned that pre-AI mostly by writing a lot of code. But if they teach newcomers to practice without AI the same would be seen as luddites.
Waiting til your 40s when you get all the benefits of the 30s plus a much more visceral feeling (e.g. back pain) that you don’t have much time left and you better be efficient about it :)
Yes probably something like tikz.dev is best.
On the flip side crafting the diagram is laborious (moving the boxes, drawing the arrows) and as such should be prime for AI boost. Isn’t there a split the difference approach where the human does the knowledge distillation into some textual description but AI generates the final diagram?
New blog post - From sets in math to types in Lean rkirov.github.io/posts/sets-v...
Leaning on AI - new blog post about using AI to learn Lean rkirov.github.io/posts/lean5/
"Is this JS function pure?" - wrote a short blog post summary of the pure JS function poll I ran in 2019
rkirov.github.io/posts/pure/
All of this should be equivalent to visualizing lambda calculus (by Curry-Howard), which opens to more visualizations/gamifications.
But which one would make the best mobile puzzle game?
[1] worrydream.com/AlligatorEggs/
[2] bntr.itch.io/visual-lambda
[3] github.com/prathyvsh/la...
Falling in an odd rabbit-hole of visualizing logical deductions.
Why isn't there a mobile friendly game for proving the ~100 core theorems of propositional and first-order logic?
[1] incredible.pm
[2] www.winterdrache.de/freeware/dom...
[3] www.jfsowa.com/peirce/ms514...
AI boosts productivity until a breaking point where domain expertise becomes unnecessary (coding, formalizing math, etc.) - you can go straight from idea to implementation without interaction with the underlying tool. Some are betting that arrives soon enough that they don’t invest in learning.
You can’t convince me Russell wouldn’t have used Lean if he had a chance.
new blog post - Why formalize mathematics - more than catching errors rkirov.github.io/posts/why_le...
Can wait to see a Fields medalist asking what’s the difference between common js and EcmaScript modules.
We got enough interest and are kicking this off this Monday 7:00pm at moxsf.com. Fill in the interest form if you would like to join us.
We got 11 sign-up so this might happen. One sign-up mistyped their email, and I couldn't reach them, so if you didn't get an email from me, please redo the form.
Next up, finding a venue.
I will consider it if I start to feel I need something that it can provide on top of my low tech tools, but also don’t want to involve more parties in this too prematurely.
Haven’t done this before, so I might be forgetting something, but only thing that comes to mind is needs a projector or a big screen.
course info - docs.google.com/document/d/1...
interest collection form - docs.google.com/forms/d/e/1F...
Calling Bay Area math enthusiasts interested in weekly sessions doing rigorous foundational mathematics the modern way - with computer-verified proofs in Lean.
(An experiment in rigorous math education outside traditional academia)
Er reals
Bad news - you have two more instances of this ahead, trichotomy of rationals and integers.
Yeah from my very limitted experience, they don’t really show up much when doing standard mathematics. Mostly lean getting stuck in dealing with universe polymorphism and one has to explicitly add universe parameters.
Do you plan to go into universes for the type system post?
But also where a new lean users needs most help due to the proliferation of tactics, with different powers and tradeoffs. So the first post would cover a lot of ground (also very dependent on the type of math one is trying to prove) but be more valuable long term.
One needs to understand the type system in order to prove anything so the second feels like a prerequisite for the first. Also from what I gather Lean types, while crazy fancy for people new to proof assistants, are a fairly standard construction. The extensibility model is where Lean shines.
Newest installment in my journey of learning how to do math proofs with computers rkirov.github.io/posts/lean4/.
On the (I hate Fins) part - I wonder if this proof in a set theory based assistant would look simper. Part of the problem is - Fins are whole types e.g. 3 in Fin 4 is very different from 3 in Fin 5. Tao suggested avoiding Fins by redefining Permutations as N -> N bijections that are id after n.
3) I am convinced this will be the only way to do math in 10-20 years, so fun to be part of the revolution as it is unfolding and maybe bring some experience from the software engineering world. These exercises are just a formal math proof version of the CS exercises we all did to learn programming.
