HackerTrans
TopNewTrendsCommentsPastAskShowJobs

reuben364

no profile record

comments

reuben364
·tháng trước·discuss
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 tháng trước·discuss
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 tháng trước·discuss
I was surprised to not see a connection made to free groups in the article.

EDIT: The wikipedia article that is.
reuben364
·8 tháng trước·discuss
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 năm trước·discuss
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.