unkz's recent activity

  1. Comment on The fall of the theorem economy in ~science

    unkz
    Link
    I think one interesting little thread that hasn’t been explored a lot is the actual capacity of human understanding. What I’m really interested in is theorems that may now be provable yet cannot,...

    I think one interesting little thread that hasn’t been explored a lot is the actual capacity of human understanding.

    The likely outcome is that formalized mathematics will now develop in two separate layers, an intelligible layer embodied by Mathlib, and an unintelligible layer we might call Mathslop, a library of results that are known to be correct via proofs that no human has ever understood.

    What I’m really interested in is theorems that may now be provable yet cannot, because of human absolute limitations, ever be completely understood by humans. Even when expressed in the most parsimonious form, the complexity may exceed human understanding. Yet, these incomprehensible proofs may yet resolve as simple statements that are themselves usable as elements of reasoning — perhaps that will be the final form of P!=NP: formally proven, yet still inscrutable.

    These elements of Mathslop may still find their way into being used in Mathlib — much like the four color theorem, where I doubt many if any people people have hand verified each of the 1500-odd cases, yet it is now universally accepted as true and used as a basis for other work.

    Perhaps someday: “If I have seen further, it is because I have stood on the shoulders of silicon giants.”

  2. Comment on Do we want to stop all crime? in ~society

    unkz
    Link Parent
    I've undergone a few significant shifts in my set of ethics, so I recognize that even what I believe right now is probably wrong in many ways and won't reflect what I think in even 5-10 years.

    I've undergone a few significant shifts in my set of ethics, so I recognize that even what I believe right now is probably wrong in many ways and won't reflect what I think in even 5-10 years.

    8 votes
  3. Comment on How to prevent mold growth under weight mats in ~life.home_improvement

    unkz
    Link
    Those look like they are almost definitely from spilled liquid. I would say, if you spill liquid immediately pull up the mats and wash/dry them, and you won’t have an issue. And maybe clean once a...

    Those look like they are almost definitely from spilled liquid. I would say, if you spill liquid immediately pull up the mats and wash/dry them, and you won’t have an issue. And maybe clean once a year — in the gym I train at we have 20 people in there soaking the mats in sweat like a slip and slide, and it’s fine. We do spray and mop the top layer after every class, and pull it all apart annually to be sure.

    4 votes
  4. Comment on What are people's experiences with using Kagi? in ~tech

    unkz
    Link
    I used to use Kagi but kind of drifted away from it. Something interesting happened though which startled me: after I stopped using it, they started emailing me saying that they noticed I stopped...

    I used to use Kagi but kind of drifted away from it. Something interesting happened though which startled me: after I stopped using it, they started emailing me saying that they noticed I stopped using it, and so they were refunding my monthly subscription fee and that they hoped I’d come back some day. So, A+ for pro-consumer behaviour.

    82 votes
  5. Comment on Is AI profitable yet? in ~tech

    unkz
    Link Parent
    I think two factors Anthropic has almost zero mindshare along casual users OpenAI is the backend of Microsoft Copilot and Github, which is everywhere

    I think two factors

    • Anthropic has almost zero mindshare along casual users
    • OpenAI is the backend of Microsoft Copilot and Github, which is everywhere
    4 votes
  6. Comment on Outsourcing plus local AI will soon become more economical vs frontier labs in ~tech

    unkz
    Link Parent
    https://developers.openai.com/cookbook/examples/reproducible_outputs_with_the_seed_parameter With the caveat that this is only mostly reproducible due to fundamental issues with parallelism. It’s...

    I recall somebody being surprised they haven't allow seeding the random number generator. This is by design, because it would make the results deterministic and you could test different models apples to apples.

    https://developers.openai.com/cookbook/examples/reproducible_outputs_with_the_seed_parameter

    With the caveat that this is only mostly reproducible due to fundamental issues with parallelism. It’s a best effort but on relatively short responses you won’t find too much drift.

    2 votes
  7. Comment on I think Anthropic and OpenAI have found product-market fit in ~tech

    unkz
    Link Parent
    People used to be able to make an argument that compilers were less efficient than hand tuned machine code, but nowadays, I’m pretty confident that all in all but the most unusual circumstances an...

    People used to be able to make an argument that compilers were less efficient than hand tuned machine code, but nowadays, I’m pretty confident that all in all but the most unusual circumstances an optimizing compiler will far outperform a human.

    What this means I think is that our best efforts from our brightest minds in the machine language space are now spent on optimizing compilers instead of writing bespoke machine code to solve individual problems.

    This is what I see in the future: we will still have high level programming experts and mathematicians who know C or Rust or high dimensional mathematics in a deep way, but their efforts will be largely focused on improving coding agents who then in turn interface with “regular” developers, like compilers or interpreted languages do today.

    5 votes
  8. Comment on I think Anthropic and OpenAI have found product-market fit in ~tech

    unkz
    Link Parent
    This is an interesting problem for sure, and I’ve spent a lot of time thinking about it. On the other hand, we used to say that about assembly language programmers.

    This is an interesting problem for sure, and I’ve spent a lot of time thinking about it. On the other hand, we used to say that about assembly language programmers.

    4 votes
  9. Comment on What are your personal crackpot conspiracy theories about the world right now? in ~talk

    unkz
    Link Parent
    I want to believe.

    I want to believe.

    1 vote
  10. Comment on What are your personal crackpot conspiracy theories about the world right now? in ~talk

    unkz
    Link Parent
    I’ve gotten the last 6 digits of my phone number several times, which really just seems impossible.

    I’ve gotten the last 6 digits of my phone number several times, which really just seems impossible.

    2 votes
  11. Comment on Weekly US politics news and updates thread - week of May 25 in ~society

    unkz
    Link Parent
    Am I OOL here? Who was arrested besides Maduro?

    the second bogus arrest of a sovereign country's leader

    Am I OOL here? Who was arrested besides Maduro?

  12. Comment on Weekly US politics news and updates thread - week of May 25 in ~society

    unkz
    Link Parent
    What does this mean?

    (but like was mostly pissed at being told what to do and he has the rights to the name?)

    What does this mean?

  13. Comment on Weekly US politics news and updates thread - week of May 25 in ~society

    unkz
    Link
    This is one of the more offensive things I have seen so far. https://aliens.gov No, it’s not about Area 51. It’s just racism. It is interesting that they straight up admit that illegal immigrants...

    This is one of the more offensive things I have seen so far.

    https://aliens.gov

    No, it’s not about Area 51. It’s just racism.

    For 60 years, the U.S. government has kept a closely guarded secret.

    Aliens have been walking among us, living in our neighborhoods, and interacting with us in our daily lives.

    They've shopped in the same stores, attended the same classes as our children, and lived seemingly normal human existences.

    With one exception — they do not belong here.

    It is interesting that they straight up admit that illegal immigrants are just like every other American. No more pretense about only deporting violent offenders.

    20 votes
  14. Comment on Who else is as excited as I am for the Backrooms movie tomorrow? in ~movies

    unkz
    Link
    I know my kids are pretty hyped, so I imagine I’ll be watching it one way or another.

    I know my kids are pretty hyped, so I imagine I’ll be watching it one way or another.

    3 votes
  15. Comment on Actually useful MCPs in ~comp

    unkz
    (edited )
    Link Parent
    Basically I have it hooked up to openclaw and obsidian, through a skill that calls Hevy MCP endpoints and the standard obsidian skill. I have five different workouts in Hevy labelled...

    Basically I have it hooked up to openclaw and obsidian, through a skill that calls Hevy MCP endpoints and the standard obsidian skill. I have five different workouts in Hevy labelled Monday-Friday. I have an obsidian document that contains my overall goals, lists of acceptable exercises. I’m integrated with telegram so every morning I get a message telling me what my workout is going to be, which is really just for fun, then I go to the gym, do the workout, sometimes leaving notes like “very easy, should increase weight”, “skipped today because rushed for time”, etc. It’s set up to poll until my workout is done and then it analyzes, proposes changes (increase reps to 12, increase weight to 60 and drop reps to 8, schedule missed exercise for Friday, etc).

    Useful stuff it’s done for me lately include reorganizing my schedule around an injury and my physiotherapist’s prescribed rehab exercises, and planning out a phased return to the gym after being out for two weeks with a tonsil infection.

    On occasion I’ll find that it’s doing something like scheduling too much or not enough and I’ll have to chat a bit about it but generally it’s well behaved. I maintain my obsidian vault in git and it has a copy of all my schedule changes just in case but I haven’t needed that backup yet.

    6 votes
  16. Comment on Actually useful MCPs in ~comp

    unkz
    Link
    Not for development but I integrate with Hevy to let an LLM manage my gym workouts. It monitors my progressive overload progression, plans around my other sports, if I miss a workout it’ll...

    Not for development but I integrate with Hevy to let an LLM manage my gym workouts. It monitors my progressive overload progression, plans around my other sports, if I miss a workout it’ll redistribute my exercises, things like that.

    7 votes
  17. Comment on If you let AI do your writing, I will come to your house and kill you in ~tech

    unkz
    Link Parent
    In principle yes, but only in a research setting. It would be cost prohibitive to do at scale.

    In principle yes, but only in a research setting. It would be cost prohibitive to do at scale.

    7 votes
  18. Comment on If you let AI do your writing, I will come to your house and kill you in ~tech

    unkz
    Link Parent
    I'm pretty aware of how language models work, having been building and training them from scratch since long before GPT even existed. I think this conflates the training objective (next token...

    I'm pretty aware of how language models work, having been building and training them from scratch since long before GPT even existed.

    because LLMs are not designed to understand the works they're trained on. They are designed to generate text that looks like the works they're trained on. That's it.

    I think this conflates the training objective (next token generation) with the learned capability: a high dimensional model of the latent structure that produced the tokens: language, concepts, facts, social patterns, relationships, and many elements of humanity in general.

    7 votes
  19. Comment on If you let AI do your writing, I will come to your house and kill you in ~tech

    unkz
    Link Parent
    Frankly, i think you are wrong. Moby Dick is also not human — it’s a bunch of paper and ink, yet it offers insight into the human condition. Why? It is also an artifact of human intellect. That is...

    AI cannot offer insight into the human condition, because AI is not human.

    Frankly, i think you are wrong. Moby Dick is also not human — it’s a bunch of paper and ink, yet it offers insight into the human condition. Why? It is also an artifact of human intellect. That is also what an LLM is, an artifact of human intellect, but one that has digested not only Moby Dick, but also millions of other artifacts of human intellect. Saying there is nothing to learn about the human condition from an LLM is like saying there is nothing to learn from going to the library.

    7 votes
  20. Comment on If you let AI do your writing, I will come to your house and kill you in ~tech

    unkz
    Link Parent
    I guess because I consume millions of tokens per day and I’m very familiar with the failure modes of these models. Hallucinations absolutely happen in complex conversations with long context...

    I guess because I consume millions of tokens per day and I’m very familiar with the failure modes of these models. Hallucinations absolutely happen in complex conversations with long context windows. This query though? The chances of it not doing a tool call to an external data provider to confirm is nil.

    9 votes