|
jcc333@jcc333.bsky.social |
@ellyzoe.bsky.social is there a branch of modal logic/proof-assistance/search that's like "you have limited attention so your lemmas have to be, in total X steps?" I'd look at Math-Wikipedia but my vocabulary is too weak to find anything like what I'm thinking of.
1 replies 0 reposts 1 likes
|
Elly
@ellyzoe.bsky.social
[ View ] |
Hey, I think you’re asking, is there a way to tell an automated proof assistant that you only want “short” proofs? I have very little experience with proof assistants, but my kid does. I’ll ask.
1 replies 0 reposts 1 likes