I'm not sure which channel is most suitable for the following in slack so I will right it here.
I thought about "informal proofs" as a concept to refer to documentation or other sources when some statements from it cannot be expressed within type-system. This proposal requires proper markdown, so I made an issue for that in YouTrack:
KT-45997 .