| CARVIEW |
Select Language
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Mon, 30 Sep 2024 18:08:52 GMT
access-control-allow-origin: *
etag: W/"66fae934-b0d"
expires: Wed, 31 Dec 2025 00:37:12 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: D94B:3FD64F:A9AD03:BEBEEA:69546DDF
accept-ranges: bytes
age: 0
date: Wed, 31 Dec 2025 00:27:12 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210073-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1767140832.077611,VS0,VE211
vary: Accept-Encoding
x-fastly-request-id: 2aeb94fc32b7605d767c4e4418b166d53bef2c67
content-length: 1284
Mario Carneiro
Hi, I'm Mario Carneiro!
I am a post-doc working in interactive theorem proving at Chalmers University of Technology.
I primarily work on the Lean theorem prover and the Metamath language, and I am the author of the Metamath Zero language. I have also done a lot of dabbling in many other languages and like to work on interaction between theorem proving languages such as HOL Light, Coq, Isabelle, and any others I can get my hands on.
Please feel free to get in touch!