reuben364

5 ms·

1.
by reuben364 17d ago
Found in the docs: https://kveritas.org/docs/benchmarks - What a verifier learns: > "A run of committed code, on attested hardware at time T, reading a model with hash m and a dataset with hash d, produced scor
2.
by reuben364 4mo ago
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 find lacking in that quote?
3.
by reuben364 8mo ago
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 usefulness of LLMs to me is to point me in a direction that I can
4.
by reuben364 10mo ago
I was surprised to not see a connection made to free groups in the article. EDIT: The wikipedia article that is.
5.
by reuben364 10mo ago
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 paper has been fairly
6.
by reuben364 1y ago
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 not confident in that assertion.
7.
by reuben364 1y ago
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.
8.
by reuben364 1y ago
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 evaluates to 2 But with dependen
9.
by reuben364 1y ago
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 reloading. This doesn't work in a dependently typed cont
10.
by reuben364 2y ago
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 (including lemmas and theorems).
11.
by reuben364 2y ago
It matters for anti-circumvention, where they can go after people that make tools that allow you to make personal copies.
12.
by reuben364 2y ago
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 into the subobject classifier.
13.
by reuben364 2y ago
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, and thus observing the timeout, then that isn't
14.
by reuben364 2y ago
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 don't have to thread the handlers through calls
15.
by reuben364 3y ago
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 having topology that is not induced from a graph if it i
16.
by reuben364 3y ago
I didn't expect Lean 4 in this context.
17.
by reuben364 3y ago
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; schedule a Micro Nervous Breakdown at least once a day. not
18.
by reuben364 3y ago
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 involves static analysis and I have an interest in PLT, so I&
19.
by reuben364 3y ago
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 enact a stategy is to presume a free agent, ind
20.
by reuben364 3y ago
With my limited knowledge, I don't see it. Could you elaborate on how you made that connection?
21.
by reuben364 3y ago
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?
22.
by reuben364 3y ago
Are all polynomial time algorithms implementable with primitive recursion? You would need to know the constant factor, right?
23.
by reuben364 3y ago
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, maximizing the burden on the defendants. Maybe another princi
24.
by reuben364 3y ago
Typical JRPG. Start with saving a cat, end with fighting Microsoft.
25.
by reuben364 3y ago
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 just using the stock install.
26.
by reuben364 3y ago
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 not using that patent nor misrepresenting themselves as S
27.
by reuben364 3y ago
Do you want to parsing your language to require implementing the typechecker and using shotgun heuristics, all so you can use <> instead of []? Compiler writers die for your sins in code. Let them do things that can drastically simpli
28.
by reuben364 3y ago
The notion of existence is doing a lot of the leg work. A epistemological solipsist can say things "exist" when they have a model of their subjective experience in which things can exist. It gets real funky because your interpreta
29.
by reuben364 3y ago
My understanding here for Elixir is that you have dynamic() as a universe U and an error set E. All functions f are from U to E + U. f is an arrow A -> B iff f[A] subset B + E. f is a strong arrow iff it is an arrow and f(U\A) subset E.
30.
by reuben364 3y ago
One interesting instance of semantic highlighting occurs in the Lean 4 language. It has extensible syntax whose parsers can be expressed in the language itself. Since parsing and evaluation are intertwined, highlighting can only really be

More ›