thevivekpandey
Joined 16 years ago
Karma
289
Submissions
77
Member since
Sep 18
A computer engineer based in Bangalore, India.
Went to IIT Kanpur, then UIUC. Worked at VMware, Google. Founded @qgraph. At Simpl in 2024.
View on Hacker NewsRecent submissions
Comment · 1 month ago
In lean, a theorem is specified by a type (in their highly complex "dependent type system") and proof is specified by a code that produces a term of that type.
If the compiler certifies that the code indeed produces a term of that type, then the proof is correct.
So, only need to trust: (1) That theorem statement is correctly encoded (FLT has a very short 1 liner description really)
(2) Lean compiler is correct