icosahedron

Same!

It's a paradigm shift, that's for sure.

I'm still in the throes of learning it myself, and it's quite the journey. I love the promises behind it, but I'm not yet far enough along to know if they are kept or if it's just kool aid (or perhaps purple drank?)

You might like looking at Dafny. It is more imperative focus, but has many of the same software proving functionality that Lean has.

It is different in that it uses SMT instead of dependent types and tactics to prove the software, but I found it more approachable.

Also, it compiles to several target languages, whereas Lean 4 only compiles to C and therefore only supports the C ABI.

It seems the repo is gone. Anyone know what happened to it?

Drawmij has teleported to another plane.

I followed the initial instructions and the 7B model worked just fine.

I tried the supplementary instructions to download some of the models (7B, 13B, and 30B), and it didn't seem to work. The prompt returned nothing after waiting for several minutes.

Is there a way to run just one of the larger models?

Congratulations on your success so far. And great job creating something useful to people in a time of need.

Ray tracer or a simple roguelike.

I've got pretty good experience with both, so knowing the algorithms is helpful. Where it gets harder isn't the language itself, but usually the idioms for expressing certain concepts.

For example, Rust doesn't have default parameters, so the builder pattern is pretty common.

Ha, as is often the case, I was making things more complicated than necessary. Jarrod got back to me quickly and let me know the err of my ways. :D

I was able to use find the author on the title page, and emailed them. I don't know if my query is incorrect or if it's a bug.

Can anyone else get beyond the 2nd level? I am getting stuck because it returns the values in slightly different order than is expected. And I don't see a way to report an issue via the website.

I do this periodically with my iPad. I use Textastic which is a decent editor with it's SSH mode.

There is also ShellFish, which is an iOS SSH file provider. You can use it to access any files via SSH as if they were from iCloud or OneDrive, etc.

Lastly, there is code-server, which is VS Code in a browser. I've used this from time to time, and it works well.

Well done. Can't wait for further chapters.

I think a table of contents is warranted. Even if it just for 3 or 4 chapters.

I didn't read as much as I normally do, mostly due to school, but I really enjoyed "The Midnight Library" and "Recursion" for fiction.

I am mostly done with Antifragile, and it's pulling me between political and philosophical sides. Don't know which side I'll land on, or how long I'll stay there.

As a side note, I've found "Deep Learning: A Visual Approach" to be very instructive.

Yeah, I hope it continues to live up to the hype you've heard. I had a hard letdown, but I hope that doesn't happen for you.