reuben364

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 score S.” If d is a public benchmark, they also confirm it is the real benchmark, without you exposing it. The score is also cross-checked by the compute-cost certificate, which confirms the evaluation consumed the compute a real forward pass over the data requires.

They should really put that front and center. Still not a complete enough description, but something at least.

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?

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 then manually verify and implement.

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 paper has been fairly easy to formalize (modulo my unfamiliarity with mathlib).

The repo is here https://github.com/badly-drawn-wizards/noperthedron

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.

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 evaluates to 2

But with dependent types, types can depend on prior values (in the previous example the type of x depends on the value t in the most direct way possible, as the type of x is t). If you redefine values, the subsequent definitions may not type-check anymore.

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 context as the type of subsequent definitions can depend on values of earlier definitions.

    def t := string
    def x: t := "asdf"
    redef t := int

redefining t here would cause x to fail to type check. So the only options are to either shadow the variable t, or have redefinitions type-check all terms whose types depend on the value being redefined.

Excluding the type-level debugging they mention, I think a lean style language-server is a better approach. Otherwise you are basically using an append-only ed to edit your environment rather than a vi.

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).

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 into the subobject classifier.

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 the case. You'd probably also want a nondetermism effect which cannot handle unless you specifically build your timeouts to be deterministic, which I think Lean 4 does, but you can't go from partial to total with it afaik.

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.

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 is at all possible.

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; schedule a Micro Nervous Breakdown at least once a day.

not sure if that is healthy though.

I guess with regards to mental health DSM type issues vs other issues, it is difficult to untangle for me. It may not be an actual disorder, but it certainly causes me distress. It's like being a science enthusiast that can't move past reading pop-sci articles (but wants to).

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've found some papers (Abstracting Abstract Machines) that I'll read through and get a rough idea. But to truly understand things I have to implement the ideas, but the scope of what I want to do expands so fast that I get demotivated and eventually move on.

Categories for the working mathematician, Software Foundations, contributing to mathlib are all things that I sort of start working towards and cannot force myself to get to any meaningful conclusion. At the same time starting so many things is how I slowly accumulated the foundations necessary to even approach these things.

It doesn't help that I also have PDA autism, which leads any sort of structure I try to impose on myself eventually becoming too stressful. I feel like I've reached the extent that modern medicine (I'm just short of max dosage of XR Ritalin) and therapy I can afford can help me.

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, individual or collective, acts according to that strategy. The act of communicating that strategy is in essence to convince those interests align with the outcome to act accordingly. We deal with imperfect information, it could be possible that someone, or a small group can unilaterally disseminate a strategy that drives wider cooperation, but those are probably unknown unknowns far too complicated to decipher by any cooperating party.

Of course this isn't it. Warp drives and luxury space communism seem to be something we could only stumble into.

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, maximizing the burden on the defendants.

Maybe another principle would be that a program is assumed to function as proven in the past. The further a given program is shown prior to be correct, the more the burden of proof shifts to the defendant to show otherwise.

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 just using the stock install.

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 Samsung screens.

https://www.youtube.com/watch?v=A002AesVaFk

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 simplify things everywhere, instead of suggesting that they're intellectually jerking themselves off. Not that they're immune to that.

EDIT: Apologies, after a bit I realized the above is a bad comment.

Separation of concerns is a common pattern in programming. It allows for things to be testable and changes to be more localized. This is an example of that.

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 interpretation of qualia results in a model that includes the brain and thus a model of how you are interpreting things as a model in your model.

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. I'm not sure how this connects to strength in the category theoretic sense.

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 effectively achieved in an LSP lest you re-implement the entirety of Lean.