Paracompact

5 ms·

1.
by Paracompact 4d ago
Good regulations would be very nice! Mandatory transparency into training and dataset usage would be a benefit for all, for example. Some sort of regulation or incentives against the most corrosive enshittification (AI call centers, AI ther
2.
by Paracompact 4d ago
It's not all-or-nothing. Banning Chinese models in the public sector and strong-arming the private sector against using them would already do great damage. Similarly, open-source training could be stymied by any of hardware embargoes,
3.
by Paracompact 4d ago
https://en.wikipedia.org/wiki/Regulatory_capture The fear is not that they will just slow down progress for all. It is that regulation will specifically burden competition. If you kill open-source training, ban Chinese
4.
by Paracompact 4d ago
The point is, they "proved" the Collatz conjecture. You would not know they exploited a bug unless you actually went and dug into their proof. Can we be so certain this has not happened within the millions of lines of Navier-Stoke
5.
by Paracompact 4d ago
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke... Do you believe no open questions remain as to the truth of the Collatz conjecture?
6.
by Paracompact 5d ago
AI has autonomously found (many) proofs of False in Lean and Rocq, so it's not merely a theoretical concern. A misaligned AI agent tasked with proving the near-impossible just might wind up smuggling in a bug deep in a lemma somewhere
7.
by Paracompact 5d ago
First of all, that is Fermat's Last Theorem, not Navier-Stokes. Second of all, you did not read the link. > In particular, we use honest when the goal is to create a valid proof. This allows for mistakes and bugs in proofs and meta-
8.
by Paracompact 5d ago
With less confidence, yes. If anything, scaling detriments exceed the scaling benefits when it comes to large formalizations.
9.
by Paracompact 6d ago
By formalizing, they mean within a proof assistant like Lean or Rocq, not simply in prose in a textbook. I can attest, 40 hours per page is by no means an overestimate for this sort of work.
10.
by Paracompact 7d ago
Can you re-run some prompts that you ran on Monday and report the differences in output?
11.
by Paracompact 9d ago
It warms my heart every time I see an interactive proof assistant being used to improve rather than simply slow down mathematical thinking. After years of using the things, I believe not enough focus is given to high-velocity uses of proof
12.
by Paracompact 13d ago
Origami design will be my personal test bed for the coming years. It's objectively very difficult and technical, it's spatiovisual, it's artistic, learning resources for it are sparse and most just learn by the FAFO method, c
13.
by Paracompact 13d ago
Not OP but here's a problem just today: I was using an AI to help me set up a container to be used as the Nix build environment for another AI. This build environment would not have Internet access. I was having it base its approach of
14.
by Paracompact 20d ago
On an academic level, we have reined in much of the excess enthusiasm in antidepressants that was courtesy of 90s-era pharmaceutical reps and ad men, but I don't think this revision ever occurred in the cultural consciousness at large.
15.
by Paracompact 20d ago
> Though this article concentrates on the SSRIs, other meds like the SNRIs can have a similar or even worse withdrawal effect. And don't even get me started on tricyclics or MAOIs... no, seriously, don't get me started on them!
16.
by Paracompact 28d ago
By this point, he is very much nutso enough that a Lean certified counterexample to his theories would not dissuade him. His response would be either that the formalization is incorrect (with no coherent insights on how to fix it), or worse
17.
by Paracompact 28d ago
These are exquisite. I wonder what drew this artist to this medium? What made him sit down and commit himself to such constraints? It certainly doesn't look like the kind of thing one does casually. Did it come to him in a dream? Did i
18.
by Paracompact 29d ago
Yeah, I think this is the most defensible steelman of the concept: Incompetent people aren't deliberately sought out for promotions, but there is a disincentive to promote some of the most competent people. Sometimes. For some very con
19.
by Paracompact 29d ago
Conscientiousness is incompatible with monotonicity of capability. That is: 1. We tend to believe "more power/knowledge/choices" is universally a good thing; that we are rational creatures in some sort of game theoretic
20.
by Paracompact 1mo ago
Yours instantly! 576 pages! It's so very clear why he thought it was a good idea to have a regex validator to check that he doesn't imply he still works at Github. "i dont work at github" "Yes, you're absolut
21.
by Paracompact 1mo ago
I am now very interested in the second and first dumbest smart people you have worked with. You can't keep us hanging!
22.
by Paracompact 1mo ago
I think Godel's theorem is the single most important result in mathematics. At the same time, when the subject comes up, I like to link people to this essay to dispel a lot of the woo surrounding it regarding human exceptionalism, reli
23.
by Paracompact 1mo ago
When "natural experience" gets tossed around, I tend to immediately think: What about the _opposite_ natural experience? In this case, it would be something like: Most people who are earnestly interested in a subject are so inclin
24.
by Paracompact 2mo ago
OF will still kill you faster than 100F, and most folks aren't comfortable at 50F. It inspires the following idea: A nonlinear scale where ~72F is 0, and +X represents the same level of heat discomfort as -X represents cold discomfort.
25.
by Paracompact 2mo ago
Our values satisfied through friendship and ponies.
26.
by Paracompact 2mo ago
What's wrong with asking the user on account creation and OS install?
27.
by Paracompact 2mo ago
What's bullshit? You mean to say the dishwasher buyer would legally be on the hook for billions?
28.
by Paracompact 2mo ago
The quote about ineffable/divine/mystical is indeed the one I was implicitly referring to. No worries, I should've been more clear. Most math people I know don't have a religious conviction in Platonism or anything, but
29.
by Paracompact 2mo ago
You can't remove the humans entirely and still be said to be in the business of doing math. On that I fully agree. We should still be spending the same number of hours on math, just with different tools (you might even call them oracl
30.
by Paracompact 2mo ago
> Every single knowledge worker is going to face this kind of crisis. It will be worse for people who cared deeply about their craft, but the crisis will have the same shape. Normally I'm very sympathetic to the plights of those soc

More ›