Viewing profile — reuben364

The quote you gave seems reasonable on it's own. ICE and Palantir comes to mind as exactly the kind of thing one would want to avoid. Could you elaborate on what particularly you f…

I find that at the granularity you need to work with current LLMs to get a good enough output, while verifying its correctness is more effort than writing code directly. The useful…

I was surprised to not see a connection made to free groups in the article. EDIT: The wikipedia article that is.

I'm working on formalizing https://arxiv.org/pdf/2508.18475 (A convex polyhedron without Rupert's property) in Lean4 I'm only on lemma 11 at this point, and up until that point the…

I'm wondering whether such syntax is subsumed by something like Lean 4 macros. I believe Lean 4 already treats binders specially in its syntax for macro hygiene reasons, but I'm no…

Since the de Bruijn indices are limited (and presumably still Turing complete), I wonder how limited you can make them and still be Turing complete.

I just wrote redef to emphasize that I'm not shadowing the original definition. def a := 1 def f x := a * x -- at this point f 1 evaluates to 1 redef a := 2 -- at this point f 1 ev…

Thinking out aloud here. One pattern that I have frequently used in EMACS elisp is that redefining a top-level value overwrites that value rather than shadowing it. Basically hot r…

There is a large library of mathematics formalized in lean called mathlib. There are graphs for the module dependencies, but I haven't seen any at the level of definitions (includi…

It matters for anti-circumvention, where they can go after people that make tools that allow you to make personal copies.

Not sure of details to make it a mathematical foundation but: A category can be defined in terms of its morphisms without mentioning objects and a topos has predicates as morphisms…

That'd almost be partial functions with extra steps. Take the Klesili category with the Maybe Monad,and you get partial functions. Unless you are manually matching on the the Maybe…

a function will return to it's call site (or diverge), a handler doesn't necessarily have to resume from where it was invoked. There is also (sort of) dynamic scoping, where you do…

I'm left confused as to what the gluing in the rule replacement is. Must the boundary of a rule match on both sides? Also what examples there would be of what an example would of h…

I didn't expect Lean 4 in this context.

At first glance that does seem to match my temperament. I love this quote as I have recently discovered it working for me If you want to think clearly, be calm and be smart; schedu…

On medication for ADHD, it helps in the short term, but I still struggle to commit to working on things in the long term. I either get bored or forget or find a new shiny. My job i…

Don't get me wrong, I agree, but aren't all solutions to problems situated in reality conterfactual to some degree. To the extent of my knowledge, isn't it all deterministic. To en…

With my limited knowledge, I don't see it. Could you elaborate on how you made that connection?

I'm having trouble getting the types right for the formula mentioned under the Matrix Function heading. Is f meant to be linear? Is f' meant to be pointwise derivative?

Are all polynomial time algorithms implementable with primitive recursion? You would need to know the constant factor, right?

Taking this to absurdity you can create a new obfuscated program for each case that presumes guilt based on whatever evidence is could be in principle be decided with a computer, m…

Typical JRPG. Start with saving a cat, end with fighting Microsoft.

When I got my SteamDeck, I thought I was going to do a lot more tinkering than I did gaming. I planned on getting NixOS working on it. I ended up just playing games and having fun …

Simultaneously, there must be harsh penalties for abusing that system. See Samsung's use of a patent on display technology to label third party displays as counterfeits, despite no…