Viewing profile — proof_by_vibes

Needed this. Thanks.

Let's see what the common denominator has to say about this!

I really think this gets at the heart of the distinction between language as it pertains to how we connect with others and language that records our observations of the world and i…

This is a very male attitude to have.

Perfectly safe. I would argue that it is the safest of the three, the least invasive both in terms of its design and in terms of privacy. The open source model of development has e…

I would not go as far to say that they exist in a bubble. I quit my job as an engineer because this exact sentiment from my boss was ruining my life.

I'll take three hours instead and hop on a train to get brunch.

I agree that it is relative, but disagree with your conclusion. I think the relativity you have in mind is what we normally think of as a setting.

Yes: https://github.com/rj-calvin/sodium The bindings are set and have a monadic interface, but there's some abstractions that still need refining/iterating: mostly I want to be ab…

I've been iterating on sodium bindings in Lean4 for about four months, and now that I've gotten to Ristretto255 I can see why the author is excited about its potential. Ristretto i…

I've been writing [libsodium]( https://doc.libsodium.org/ ) bindings in Lean4 and have ended up using `native_decide` quite liberally, mostly as a convenience. Can any Lean devs pr…

This is perfect. I'm currently creating a MUD and these are exactly the kind of fonts I want. Thanks for sharing!

Are there any experts that could help me bootstrap myself on the current literature on "world models?"

I'm of the opinion that formalization is the biggest bottleneck of current generation LLMs. However, I don't think that this necessarily suggests that LLMs don't benefit from forma…

Finally I find this argument. Agreed, and I'm baffled that people think that AI is what's going to "solve loneliness." Loneliness has already been solved by YouTube/Twitch. The bra…

As a playwright, I've certainly thought about AI impacting the art. In fact, it was the very eloquence of chatgpt's output that initiated all of this mania in the first place: not …

Testing in general is quickly being outmoded by formal verification. From my own gut, I see software engineering pivoting into consulting—wherein the deliverables are something aki…

Not necessarily. Theorem provers provide goals that can serve the same function as "debug text." Instead of interpreting the natural language chosen by the dev who wrote the compil…

Related to linear programming in theorem provers is this paper on Farkas' lemma implemented in Lean. It doubles as an interesting onboarding for working with some of the common abs…

There could be merit to this. Proofs are generally computationally hard, so it's possible that a currency could be created by quantifying verification.

Speak for yourself. I've got $10mil riding on put options for Jane Doe's pizza that she bought for her child's birthday party last week. People like you spreading FUD is threatenin…

Never underestimate the power of shame on the human psyche. Many would rather double down on the "reality distortion field" than to admit wrongdoing or poor judgement.

I would argue there is merit in keeping a platform separate for the purpose of education. Humans shape their tools that in turn shape themselves. In a general purpose theorem provi…

Some additional context: https://lean-lang.org/theorem_proving_in_lean4/axioms_and_co... Also, a github link for those who don't want to use a google account: https://github.com/rj…