HackerTrans
トップ新着トレンドコメント過去質問紹介求人

reuben364

no profile record

コメント

reuben364
·先月·議論
The quote you gave seems reasonable on it's own. ICE and Palantir comes to mind as exactly the kind of thing one would want to avoid. Could you elaborate on what particularly you find lacking in that quote?
reuben364
·6 か月前·議論
I find that at the granularity you need to work with current LLMs to get a good enough output, while verifying its correctness is more effort than writing code directly. The usefulness of LLMs to me is to point me in a direction that I can then manually verify and implement.
reuben364
·8 か月前·議論
I was surprised to not see a connection made to free groups in the article.

EDIT: The wikipedia article that is.
reuben364
·8 か月前·議論
I'm working on formalizing https://arxiv.org/pdf/2508.18475 (A convex polyhedron without Rupert's property) in Lean4

I'm only on lemma 11 at this point, and up until that point the paper has been fairly easy to formalize (modulo my unfamiliarity with mathlib).

The repo is here https://github.com/badly-drawn-wizards/noperthedron
reuben364
·5 年前·議論
Adding more fuel to the fire is that most of the benefit in learning the underlying principles of software is being able to build, modify and introspect it. In a terminal, to view a text file, you could use cat. On a phone, you download an app. However, you can't pipe your Free TXT Viewer 2000 to another app (and if you could, it would probably inject ads). As the walled garden closes in, the incentives to learn diminish as being able to accomplish anything with such acquired knowledge will be severely limited.