Hacker Newsnew | past | comments | ask | show | jobs | submit | richard_chase's commentslogin

Anyone know of a good Lean tutorial? I've played around with it a bit but never really learned it properly.

Why do I need to use this? Why can't I just use the LLMs directly to generate lectures if I want?


You can attempt to do it, but you'll see that it won't work. We've built the underlying "lectures as code" technology to make this work.


You just said in another comment that you use Claude Opus 5 to generate the video in a single shot. What about it won't work?


We ask Claude Opus 5 to write a specific kind of source code that only our proprietary software understands and can render into a lecture video with computer graphics and TTS.

Without our system, there isn’t really an equivalent target language you can ask the LLM to write. Manim exists, but you won’t get videos like these by simply asking an LLM to generate Manim code.


That's right, just give me the prompt, not the LLM output, and I will prompt my own model! I would rather read the millions of tokens that went into the prompt than watch a video, and I am sure all other students would too.

Just assign years worth of reading homework every week, and I am sure all the students will fulfill their assignments of reading every token that went into each video, no matter how many, rather than watch an LLM generated video.

Students simply need to learn how to read text as fast as an LLM can, and have an enormous token budget to use the LLMs directly themselves.

And while you're at it, increase their tuition by the amount those tokens cost, so each student can pay for feeding the same tokens into their own LLM instead of the school doing it once and paying out of their own pocket immediately. Because the idea of schools producing reusable courseware is unprecedented! That way they can fold the token cost into their student loans.

Sarcasm off. Here is what I actually mean, and I think it makes a better case for this than the authors made for themselves.

The prompt is not "give me a lecture on relativity." That is only the part you type. The rest is the lecture description language, the visual grammar, the worked examples, the pedagogical constraints, and the review loop: a program, not a request. Latent training gives you the physics for free. It does not give you the presentation. Asking why you need this when you have an LLM is like asking why you need a compiler and a library when you already have a CPU.

Authoring cost is paid once and amortized over every viewer. That is what a textbook is. "Just prompt it yourself" is the scriptorium: every student copies their own book, pays their own tokens, and collects their own transcription errors. A school paying once and shipping one reviewed artifact to everybody is not a limitation, it is the entire point of courseware.

Their strongest argument is the one they undersold: the source is the artifact. Every recorded lecture on the internet is a render, frozen and unpatchable, and its mistakes are permanent. If the lecture is source code, a mistake becomes a patch, a translation becomes a recompile, and improvements accumulate instead of being lost every time someone re-records from scratch. And because they render deterministically from source with graphics and TTS instead of generating video with a diffusion model, a fix is a fix and not a re-roll. That is the real correctness argument, and it never got made.

Graphics settled this exact split forty years ago. PostScript is the authoring language: loops, conditionals, a full interpreter. PDF is PostScript with the programming removed, an inert render of flat drawing calls with all the loops unrolled, and Distiller produces one from the other by running the program and recording what it draws. Language in the middle, inert artifact at the edge. A lecture wants the same shape, and "lectures as code" is that observation applied to teaching.

Other arguments available to them: a lecture with a git history is a new kind of object, because you can bisect an explanation and read the changelog of a proof. Errata stop being a sheet nobody reads and become a rebuild. Localization, transcripts, and accessibility fall out of the source instead of being bolted onto a render. One source can emit different levels, and different notation conventions for physicists and mathematicians.

The answer to davisp lives in the same place: sign the source. Feynman is trusted because his lectures are texts we can check, argue with, and cite. Publish the language, publish the sources, publish the diffs, let critics file issues against a named maintainer, and "everyone who watches after the fix gets the corrected lecture" becomes a checkable claim instead of a promise. That's the one thing they're not doing. regnull asked for the language and was told it is the company. Right now they keep the LaTeX and the PostScript and ship only the PDF -- and they're PhD students! arXiv wants their .tex, not just their PDF, because in their own field shipping only the render was never good enough.


"Linear Algebra and Its Applications" by David Lay is the best introductory linear algebra textbook, hands down. Love it.


I had this as my very first textbook in community college. Loved it!


I hear recommendations for this book all the time; I've cover-to-covered Strang several times and have digested maybe 20% of Axler (I just dip into random sections of LADR when something annoys me in a problem set or whatever), and I'm super curious why the aura on Lay's book is so positive.

(I don't doubt it at all! I'm just curious.)


As someone who's watched all Strang's lectures and read most of Axler's book, I found Linear Algebra and Its Applications to give the most interesting treatment on the topic. What made it so special was its clear explanations and the use cases it introduced.

The applications not only provided the context to get a deeper understanding of the concepts, it also made the math relevant to the real world. By showing a range of problems, from the chemical stoichiometry to the algorithmic SVD, it inspires the reader to look for more problems that can be solved with the toolset being introduced.


Lay explains things very clearly and it's very good for going back to when I need to review something. Lay covers all the foundational linear algebra topics you would need for say, ML or graphics programming. I found that roughly the first half of LADR felt like a review of what Lay covered.


You won't get anything new from Lay's book if you've done Strang. It is a basic textbook and doesn't cover anything advanced. It's just a good textbook.


I think Stewart's Calculus is excellent and it is rightfully the standard textbook. No modifications needed in my opinion.


James Stewart made a lot of money off his textbook.

Here is an article about the interesting house he designed:

https://torontolife.com/real-estate/look-inside-integral-hou...


Which book is that exactly? I'm finding lots of calculus book for "Stewart's Calculus" :(


Calculus by James Stewart, Daniel Clegg, and Saleem Watson

https://www.stewartcalculus.com


James Stewart is the author, there are 8 or 9 edition of the same book. Any will do.


That means the post was good, even though the blurry math images are illegible. But yes, as a Fields medalist he is an expert on LLMs.


> But yes, as a Fields medalist he is an expert on LLMs.

Not what I was claiming, but since you are, feel free to expand on this.


I like this counterexample technique against sarcastic comments, I should try it next time someone writes a dismissive comment.


You could try it but I don't think it's going to work. Go ahead, try it.


The Fields medal is awarded to those who are the best at using LLMs (e.g. vibe-coding Lean) and those with the best WordPress blog with blurry math images. It is a huge honor in the vibe-coding community.


Good stuff. Maybe I missed it in the post, but I didn't see a formal proof of the conjecture?


Follow the link to the chat history. The last item is a full write up.


Yes, and the standalone formal proof and independent review will follow.

By the way, I'd like to note that it will likely be a formalization of not the last result in that conversation, but of one of the initial proofs that relied on the Langford sequences and theorems of their existence.


I think the new generation will be alright. From what I've seen, they seem to believe that maximizing their looks is the answer.


That is a thing people do when they feel a lack of control over other aspects of their life. It's a coping mechanism. Frequently comorbid with depression.

Also it's quite rude of you to dismiss an entire generation with this belittling rhetoric. Mental health is a really, really big deal.


Watch any movie, typically the protagonist is good looking and antagonist is ugly. That's the whole answer.

In Game of Thrones director had a chance to make the dwarf (protagonist ) really ugly, like in the books, but they chose a good looking actor.

Same for Harry Potter, Hermione was supposed to be meh.


I think the previous generation of Hollywood films was not so egregious on this. There were a lot of normal looking famous actors: Bill Murray, Jack Nicholson, Robert De Niro etc. Often playing good guys.

Now most actors in popular media are good looking to an uncanny level. Antagonist are beautiful too (in GoT as well).

It's not surprising if this negatively affects the psyche of the everyday person.


That's absolutely not the whole answer and never has been.

- People who crave validation seek good looks. They want to be accepted.

- People who crave status seek good looks. They want to be awarded.

- People who crave admiration seek good looks. They want to be desired.

There are so, so many more possible reasons and motivations, and it highly depends on the individual. Someone could have all of the above or none of the above and still obsess over looks. Someone could obsess for different reasons in different contexts or with different moods.

It's not based on some infantile monkey-see-monkey-do obsession with media.


Yes, but if they only see the people of their small town, they see averages, and get a better idea of their own looks, than if they see best shots of the best actors online/in movies.


It feels almost disingenuous to claim it's solely caused by beauty standards.


Calhoun's mouse utopia experiment is looking more and more real by the day.

> The "Beautiful Ones": Younger mice withdrew entirely from social interaction, spending all day grooming and eating alone without mating or fighting.

> Hyper-Aggression and Apathy: Dominant males attacked others randomly, females neglected or killed their young, and reproduction completely flatlined.

Remind you of anything?


Looks and feels super vibe-coded.


how do you categorize 'super' and just vibecoded x'D


This looks like they just accepted the first thing Claude gave them.


It would have been funny to get a cookie banner on this site. They missed a good opportunity.


I'm all for this. I don't think mathematics should be done as a profession. If you can't find free time to do it, it's obviously not that important to you. Open source software works pretty well, doesn't it? Why not math?


> If you can't find free time to do it, it's obviously not that important to you. Open source software works pretty well, doesn't it? Why not math?

You do realize that much of a number of vital open source projects are primarily developed by people who are paid to develop it?

> I don't think mathematics should be done as a profession.

Personally, I don't think writing, blogging, acting or singing should be a profession either. But here we are.


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: