@_torayuri

All good! Thanks for asking

@kooi5 notes10 replies1 tag, 0 users following1 followerNo bio yet.enter to follow4d · 1 replyenter to reply

How are things wrapping up?

:((

@catastrofer9 notes8 replies0 tags, 4 users following3 followersJust another AI guyenter to follow5d · 1 replyenter to reply

I hatw Sunday evening anxiety :(, man seriously wtf?

Good day

(deleted)

At least rate limiting! (as I'm posting this I hit the limit of 3 posts every 5 minutes, good!)

@bobby6 notes6 replies0 tags, 0 users following2 followersNo bio yet.enter to follow6d · 12 repliesenter to reply

any ideas on how to prevent ai-generated stuff on this platform?

I can't think of a good way to also prevent that kind of solutions and ended up prompting "please don't enumerate and filter". Opus 4.7 then reimplemented and proved the backtracking algorithm.

@_torayuri3 notes8 replies0 tags, 1 user following1 followeri create thingsenter to follow6d · 1 replyenter to reply

In the first attempt, Opus 4.7 successfully completed it and proved it. However, the solution is to enumerate all possible space and .filter out anything that doesn't qualify my definition, which is obviously not ideal (if cheating is too harsh).

In the first attempt, Opus 4.7 successfully completed it and proved it. However, the solution is to enumerate all possible space and .filter out anything that doesn't qualify my definition, which is obviously not ideal (if cheating is too harsh).

@_torayuri3 notes8 replies0 tags, 1 user following1 followeri create thingsenter to follow6d · 2 repliesenter to reply

OK. I've translated the (correctness) requirements of LeetCode No.22 to Lean, and ask Claude Code to both implement a solution and prove it.

I remember seeing a CLI microblog project some years ago..

@hjkl2 notes1 reply0 tags, 0 users following1 followerNo bio yet.enter to follow6d · 1 replyenter to reply

A CLI would ve good for this

The two projects of github:schildep are "3d mesh intersection" and "multipolygon intersection". I can try "Voronoi diagram generation" as a starter.

@_torayuri3 notes8 replies0 tags, 1 user following1 followeri create thingsenter to follow6d · 1 replyenter to reply

Inspired by two projects of github:schildep I start to explore what can be expressed in Lean and make coding agents implement and prove the implementation at the same time.