lg5689

5 ms·

1.
by lg5689 27d ago
IANAL, but yes, I'd assume the license is unenforceable on the AI content.
2.
by lg5689 27d ago
No, an AI's output can still violate copyright.
3.
by lg5689 1mo ago
LLMs are indeed very special compared to past efforts at automated theorem proving. The search tree for proofs is enormous, even short textbook exercises (i.e. a few dozen lines of Lean) were difficult with GOFAI techniques. Adding a few or
4.
by lg5689 2mo ago
There was recently an announcement that a group trying to formalize it found a gap exactly where other mathematicians were pointing. So to the extent there was any doubt, it should be gone now--the proof was incorrect. But I agree LLMs have
5.
by lg5689 3mo ago
I believe that "single source of truth" is a principle that should always be followed. If there's duplicated code where it'd be a bug if they diverge, then you should refactor. It creates a long-distance coupling in your
6.
by lg5689 4mo ago
One of the authors said in a reddit comment (and I hope I am summarizing accurately) that it's impossible to show a diagram as the smallest instance of the technique gives like 10^1000000 points.
7.
by lg5689 4mo ago
The problem was pretty well known, and had many human attempts. There's some room to argue that the right humans hadn't attempted it, as the solution used advanced methods from another field of math. But imho, whereas many prior A
8.
by lg5689 4mo ago
This is happening to other forms of competitive programming too. The most recent AIs have problem solving skills rivaling top humans, and so if AI can't be easily banned, the competition is dominated by AI agents. I thought code golf w
9.
by lg5689 7mo ago
You can't do this for general functions, but it's fine to do in cases where the definition of f naturally embeds into the rationals. For example, a polynomial over Z is also a polynomial over Q or C.
10.
by lg5689 7mo ago
The movement from R to C can be done rigorously. It gets hand-waved away in more application-oriented math courses, but it's done properly in higher level theoretically-focused courses. Lifting from a smaller field (or other algebraic
11.
by lg5689 7mo ago
You can go farther and say that you can't even construct real numbers without strong enough axioms. Theories of first order arithmetic, like Peano arithmetic, can talk about computable reals but not reals in general.