Paracompact

4 ms·

1.
by Paracompact 5d ago
Elon's mother recently posted an AI-generated photo of her son's birthday party. The tag indicating such was scrubbed as soon as it was pointed out.
2.
by Paracompact 7d ago
> Anyone who is even quite intelligent but has really pursued the rigorous stuff, unless they are in fact a prodigy, eventually realizes they have an abstraction ceiling Eh. I'm a math PhD who fled academia because it was too much f
3.
by Paracompact 7d ago
Another response to math that makes me sad: "I must be too stupid to understand this," "my brain is too small for this," etc. Different people say it for different reasons, but it's almost always in response to a ha
4.
by Paracompact 8d ago
If there is any barrier, it is not intentional, I assure you. Math is just hard.
5.
by Paracompact 9d ago
"This is the business we've chosen."
6.
by Paracompact 13d ago
It was trivial because the Collatz proof script is literally 1000x smaller than the script for Navier-Stokes and involves no advanced math. And they found the bug by... manually inspecting the proof script. Maybe we should do the same for
7.
by Paracompact 13d 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
8.
by Paracompact 13d 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,
9.
by Paracompact 13d 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
10.
by Paracompact 13d 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
11.
by Paracompact 14d 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?
12.
by Paracompact 14d 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
13.
by Paracompact 14d 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-
14.
by Paracompact 15d ago
With less confidence, yes. If anything, scaling detriments exceed the scaling benefits when it comes to large formalizations.
15.
by Paracompact 16d 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.
16.
by Paracompact 16d ago
Can you re-run some prompts that you ran on Monday and report the differences in output?
17.
by Paracompact 19d 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
18.
by Paracompact 22d 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
19.
by Paracompact 22d 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
20.
by Paracompact 29d 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.
21.
by Paracompact 29d 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!
22.
by Paracompact 1mo 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
23.
by Paracompact 1mo 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
24.
by Paracompact 1mo 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
25.
by Paracompact 1mo 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
26.
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
27.
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!
28.
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
29.
by Paracompact 2mo 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
30.
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.

More ›