proof_by_vibes (u/proof_by_vibes)

proof_by_vibes commented on We may not like what we become if A.I. solves loneliness newyorker.com/magazine/20... · Posted by u/defo10

bowsamic · a month ago

I honestly just think it’s that before there was so little to do at home that you were just bored as hell if you didn’t go out. Now there’s just infinite entertainment of all kinds

proof_by_vibes · a month ago

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 brain is easily tricked into thinking that it is "being social" when it is subject to the effects of the parasocial relationships that are formed by these platforms. People's afternoons are rapidly becoming consumed by hours of YouTube where they come out of it with a brain telling them: "boy, that's enough social interaction for today!" Introversion has become an epidemic as a result.

proof_by_vibes commented on AlphaWrite: AI that improves at writing by evolving its own stories tobysimonds.com/research/... · Posted by u/tamassimond

proof_by_vibes · 3 months ago

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 only was chatgpt able to explain to me gauge theory with surprising accuracy, it was able to do so using perfect Elizabethan english—exactly as I had instructed it to.

There is a missing ingredient that LLMs lack, however. They lack insight. Writing is made engaging by the promise of insight teased in its setups, the depths that are dug through its payoffs, and the revelations found in its conclusion. It requires solving an abstract sudoku puzzle where each sentence builds on something prior and, critically, advances an agenda toward an emotional conclusion. This is the rhetoric inherent to all storytelling, but just as in a good political speech or debate, everything hinges on the quality of the central thesis—the key insight that LLMs do not come equipped to provide on their own.

This is hard. Insight is hard. And an AI supporter would gladly tell you "yes! this is where prompting becomes art!" And perhaps there is merit to this, or at least there is merit insofar as Sam Altman's dreams of AI producing novel insights remain unfulfilled. This condition notwithstanding, what merit exactly do these supporters have? Has prompting become an art the same way that it has become engineering? It would seem AlphaWrite would like to say so.

But let's look at this rubric and evaluate for ourselves what else AlphaWrite would like to say:

```python # Fallback to a basic rubric if file not found return """Creative writing evaluation should consider: 1. Creativity and Originality (25%) - Unique ideas, fresh perspectives, innovative storytelling 2. Writing Quality (25%) - Grammar, style, flow, vocabulary, sentence structure 3. Engagement (20%) - How compelling and interesting the piece is to read 4. Character Development (15%) - Believable, well-developed characters with clear motivations 5. Plot Structure (15%) - Logical progression, pacing, resolution of conflicts""" ```

It's certainly just a default, and I mean no bad faith in using this for rhetorical effect, but this default also acts as a template, and it happens to be informative to my point. Insight, genuine insight, is hard because it is contingent on one's audience and one's shared experiences with them. It isn't enough to check boxes. Might I ask what makes for a better story: a narrative about a well developed princess who provides fresh perspectives on antiquated themes, or a narrative about a well developed stock broker who provides fresh perspectives on contemporary themes? The output fails to find its audience no matter what your rubric is.

And here lies the dilemma regarding the idea that prompts are an art: they are not. The prompts are not art by the simple fact that nobody will read them. What is read is what all that is communicated and any discerning audience will be alienated by anything generated by something as ambiguous as a English teacher's grading rubric.

I write because I want to communicate my insights to an audience who I believe would be influenced by them. I may be early in my career, but this is why I do it. The degree of influence I shall have measures the degree of "art" I shall attain. Not by whether or not I clear the minimum bar of literacy.

proof_by_vibes commented on AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms deepmind.google/discover/... · Posted by u/Fysi

mattlondon · 4 months ago

"Coding" might be solved, but there is more to software engineering than just churning out code - i.e. what should we build? What are the requirements? Are they right? Whats the other dependencies we want to use - AWS or GCP for example? Why those and not others - whats the reason? How does this impact our users and how they use the system? What level of backwards/forwards compatibility do we want? How do we handle reliability? Failover? Backups? and so on and so on.

Some of these questions change slightly, since we might end up with "unlimited resources" (i.e. instead of having e.g. 5 engineers on a team who can only get X done per sprint, we effectively have near-limitless compute to use instead) so maybe the answer is "build everything on the wish-list in 1 day" to the "what should we prioritize" type questions?

Interesting times.

My gut is that software engineers will end up as glorified test engineers, coming up with test cases (even if not actually writing the code) and asking the AI to write code until it passes.

proof_by_vibes · 4 months ago

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 akin to domain-specific languages that are tailored to a client's business needs.

proof_by_vibes commented on AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms deepmind.google/discover/... · Posted by u/Fysi

j2kun · 4 months ago

This just means that it operates on the (debug text form of the) intermediate representation of a compiler.

proof_by_vibes · 4 months ago

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 compiler, these goals provide concrete, type-accurate statements that indicate the progress of an ongoing proof.

proof_by_vibes commented on A tool to verify estimates, II: a flexible proof assistant terrytao.wordpress.com/20... · Posted by u/jjgreen

proof_by_vibes · 4 months ago

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 abstractions found in Mathlib: https://github.com/madvorak/duality/blob/main/nonLean%2Fdual...

proof_by_vibes commented on Intellect-2 Release: The First 32B Model Trained Through Globally Distributed RL primeintellect.ai/blog/in... · Posted by u/Philpax

iTokio · 4 months ago

It’s interesting that it does something useful (training a LLM) without trust and in a decentralized way.

Maybe this could be used as proof of work? To stop wasting computing resources in crypto currencies and get something useful as a byproduct.

proof_by_vibes · 4 months ago

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

proof_by_vibes commented on Burrito Now, Pay Later enterprisevalue.substack.... · Posted by u/gwintrob

pxndx · 4 months ago

Absolutely unhinged content from someone who needs to touch grass. Payday loans are scams that prey on the poorest, most uneducated people. This industry is actively harmful to society. But hey, I'm sure writing this helps you sleep at night.

proof_by_vibes · 4 months ago

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 threatening my portfolio.

proof_by_vibes commented on U.S. Economy Contracts at 0.3% Rate in First Quarter wsj.com/economy/us-gdp-q1... · Posted by u/bko

Gimpei · 4 months ago

I’m curious if any Trump voters are starting to feel any buyer’s remorse. The pain from the tariffs is only going to get worse. Soon we will have Trumpflation and a Trumpcession. Meanwhile, auto manufacturers are laying off employees. We are seeing pain with no gain. There is no reindustrialization nor will there ever be through this policy. For every economist except for Navarro, this is quite the own goal. I’m guessing you all were expecting Trump 1. Any doubts creeping in yet?

proof_by_vibes · 4 months ago

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.

proof_by_vibes commented on A proof checker meant for education jsiek.github.io/deduce/in... · Posted by u/alabhyajindal

rendaw · 5 months ago

> A proof checker meant for education

What makes it for education? Why can't it be used as a general purpose proof checker?

proof_by_vibes · 5 months ago

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 proving environment, such as with Lean, there is a different attitude about what level of abstraction to expose by default. It's less intuitive to a child to have a tutor need to explain what it means for a function to be `unsafe` than it is to explain what it means to `print` an expression.

By creating a separate platform, you can set these defaults to curate different kinds of engagement with users. Take the `processing` language as an example. While it's Java under the hood, the careful curation of the programming environment incentivizes learners to play with it like a toy, increasing creative expression and fault-less experimentation.

proof_by_vibes commented on Verisimilitude: The Structure and Interpretation of Narratives drive.google.com/file/d/1... · Posted by u/proof_by_vibes

proof_by_vibes · 5 months ago

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-calvin/verisimilitude/blob/069723c94df...