Do you have a link? That might mean a set of different things, ranging from very hard to impossible; strictly speaking, this seems to go against Godel's theorem

Do you have a link? That might mean a set of different things, ranging from very hard to impossible; strictly speaking, this seems to go against Godel's theorems tho there are standard workarounds. I'm familiar with https://coq.discourse.group/t/alpha-announcement-coq-is-a-lean-typechecker/581 https://coq.discourse.group/t/alpha-announcement-coq-is-a-le..., which was just hard, but it does not prove Lean consistent, it only lets Coq process the Lean stdlib.