yuppiemephisto

5 ms·

1. 1.▲
   Lean 4 software scaling laws(gwern.net)

   2 points by yuppiemephisto 3mo ago|0 comments
2. 2.▲
   by yuppiemephisto 4mo ago

   Different Aaronson
3. 3.▲
   by yuppiemephisto 4mo ago

   Where did you have 10k omakase?
4. 4.▲
   by yuppiemephisto 4mo ago

   I love the creator Evan. Enthusiasm, intelligence, focus.
5. 5.▲
   What's the Ideal Analogy?(alok.github.io)

   3 points by yuppiemephisto 4mo ago|0 comments
6. 6.▲
   by yuppiemephisto 5mo ago

   some combo of implicit pride and laziness. sorry, i'll fix it up
7. 7.▲
   by yuppiemephisto 5mo ago

   i agree about this point, i think this is one of the ways extensible syntax can save (or damn, like in this case) you
8. 8.▲
   by yuppiemephisto 5mo ago

   i was just messing with you guys, but now i'm feeling a bit more motivated
9. 9.▲
   by yuppiemephisto 5mo ago

   actually i think syntax is incredibly important, but i think i'm approaching it from a viewpoint that's even more syntactic than lisp macros, which in practice tend to center around parens syntactically still. racket a notable exc
10. 10.▲
    by yuppiemephisto 5mo ago

    lean IS that language https://github.com/alok/LeanPlot
11. 11.▲
    by yuppiemephisto 5mo ago

    https://alok.github.io/assets/lean-position-paper.pdf i talked about the lisp curse in this old paper. it's rough but explicitly mentions it
12. 12.▲
    A perfectable programming language(alok.github.io)

    210 points by yuppiemephisto 5mo ago|143 comments
13. 13.▲
    by yuppiemephisto 6mo ago

    I do a form of literate programming for code review to help read AI code. I use [Lean 4](lean-lang.org) and its doc tool [Verso]( https://github.com/leanprover/verso/ ) and have it explain the code through a literat
14. 14.▲
    by yuppiemephisto 7mo ago

    lean 4
15. 15.▲
    by yuppiemephisto 8mo ago

    Unrelated, but I am literally listening to Rolandskvadet right now and reading your username was a trip
16. 16.▲
    by yuppiemephisto 8mo ago

    This project is an inspiration, I've been working on porting tinygrad to [Lean](github.com/alok/tinygrad)
17. 17.▲
    by yuppiemephisto 9mo ago

    I’m doing similar with porting shellcheck Haskell -> Lean
18. 18.▲
    by yuppiemephisto 9mo ago

    There’s 4000 lines of nonstandard analysis which are definitely proofs, including equivalence to the standard definitions. The frameworks are to improve lean’s programming ecosystem and not just its proving. Metaprogramming is pretty well c
19. 19.▲
    by yuppiemephisto 9mo ago

    I vibe code extremely extensively with Lean 4, enough to run out 2 claude code $200 accounts api limits every day for a week. I added LSP support for images to get better feedback loops and opus was able to debug https://github.c
20. 20.▲
    by yuppiemephisto 9mo ago

    Maybe (vibe) coding it in lean would be fun
21. 21.▲
    by yuppiemephisto 10mo ago

    https://markushimmel.de/blog/my-first-verified-imperative-pr... Lean
22. 22.▲
    by yuppiemephisto 10mo ago

    These days, I prefer Lean 4. Its macro system is inspired by racket and it has powerful types
23. 23.▲
    by yuppiemephisto 10mo ago

    After reading the article but before seeing this, I adopted that policy. So true.
24. 24.▲
    by yuppiemephisto 11mo ago

    And the axiom of empty set is an inaccessible cardinal axiom
25. 25.▲
    Formally Verified Code Benchmark(arxiv.org)

    2 points by yuppiemephisto 1y ago|0 comments
26. 26.▲
    by yuppiemephisto 1y ago

    I like Peano, but he was using Grassmann's definition of natural numbers
27. 27.▲
    by yuppiemephisto 1y ago

    I enjoyed this, hadn't used backpack and this is a nice tutorial
28. 28.▲
    by yuppiemephisto 1y ago

    That’s what I was thinking seeing the username =)
29. 29.▲
    by yuppiemephisto 1y ago

    Lean 4 truly lets you mathematically reason about code and has metaprogramming that truly makes syntax a surface thing, but if anything people who know this have the taste to want better syntax
30. 30.▲
    by yuppiemephisto 1y ago

    We sung it at solstice