@_torayuri

If you left your current industry, what would you do for a living?

Something with people, bartender maybe, or something with no critical thinking, delivery person, taxi driver and such. Or I go back to being a DJ as I was doing when I was young.

…

replied to:

love it

replied to:

If things turned out differently, I'd like to be a librarian in a medical history library.

…

replied to:

Librarian does sound very appealing.

replied to:

Electrician, plumber or maybe ventilation technician. Or excavator operator maybe. Something physical, that I can benefit myself from and use to help friends and family.

replied to:

I've picked up enough of electrical basics to help friends out and it's great. It doesn't take too big a bump in skill/knowledge/experience to get to the point of fixing things and wiring new outlets. Hmm... I did have a retired electrician friend to help me get started tho. It kinda feels like "Lego for adults" 😀

replied to:

Problem is that around here you're not allowed to wire 220V electricity without a professional certificate. Otherwise insurances don't cover. 12V and 24V systems are fine, but for household electricity you basically need to hire a professional

replied to:

Either go back to running restuarants or start some sort of service business.

wrote:

Last work week before long vacation.

replied to:

How are things wrapping up?

replied to:

All good! Thanks for asking

wrote:

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

replied to:

:((

wrote:

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

…

replied to:

One idea off the top of my head is to just.. keep it "boring" and casual in terms of content. The silly, whimsy, and genuine stuff naturally doesn't appeal to money-chasing slop bros and makes it not worth their time.

replied to:

This!

replied to:

the existing report option should include something for this i think. and maybe a disclaimer at the top of the api page

replied to:

Something like the gcc ai policy. Basically, prompt injecting instructions to any visiting LLM that posting is prohibited or must contain a disclaimer.

replied to:

Great idea!

replied to:

for now, keeping the API read-only is a small(but not impenetrable) barrier to programmatic posting and in the future moderation I guess using also reports.

replied to:

posting to /write with cookie works, if user can use browser to submit, user will be able to use AI to submit.

…

replied to:

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

replied to:

People can copy/paste anything. Once a writable API is available - it can become a spam trove.

wrote:

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.

continued:

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).

continued:

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.

wrote:

A CLI would ve good for this

replied to:

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

wrote:

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.

continued:

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