Skip to content

Comment on Some Junk Theorems in Leanparent

Comments

This was helpful, thanks.

the last paragraphs cite why junk theorems are objectionable but then fully misinterprets it to draw the opposite conclusion. the intersection is the S-feature and problematic. 1 + 2 = 4 is a “theorem beyond T” expressed in T theory.

don’t be mislead about what a junk theorem is!

Thank you. I was following along until that paragraph and got the opposite interpretation too.

Yah, I read that and thought "this seems like gibberish: maybe I am reading LLM slop".

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.