hello!

Stream: new members

[Trevor Murphy]

Hey folks! :wave: I'm a math grad student just getting into lean. I've enjoyed working through the "Mathematics in Lean" documentation and I'm learning more by formalizing some of my recent homework problems. I've already solved one of my issues in the process of typing up a question for this chat :sweat_smile: so I'm looking forward to hanging out here more over the holidays

[NAJIH]

Hi everyone,

I’m new here and would like to share a small Lean project.

The project explores a formation-level typing constraint between
syntactic entities (codes, quotations, descriptions)
and propositions.

Key point:
Prop in Lean is a proof-theoretic type, not automatically a semantic
truth-bearer. Lifting a syntactic object to something treated as a
proposition requires an explicit, well-typed coercion.

Under this constraint, classical self-referential constructions
(e.g. Liar-style / Gödel-style descriptions)
fail to form as valid propositions — Lean blocks them as ill-typed
at formation time.

The Lean files are complete and fully type-check.

Repo:
https://github.com/najih7777777-cpu/pre-semantic-type-validation

Any technical feedback is very welcome.