estoy-re-sebado's blog

By estoy-re-sebado, history, 13 months ago, In English

Several months ago I came across an online judge, IIRC called Mathforces, that let you submit [Lean](https://en.wikipedia.org/wiki/Lean_(proof_assistant)) proofs for math problems.

The problem is I can't seem to find it anymore. Does anyone know what came of it? And if it's still online, what the current URL is? Or if you know who created it, how to get in contact with them?

  • Vote: I like it
  • +35
  • Vote: I do not like it

»
13 months ago, hide # |
← Rev. 2  
Vote: I like it -8 Vote: I do not like it

.

  • »
    »
    13 months ago, hide # ^ |
     
    Vote: I like it 0 Vote: I do not like it

    I don't think that's it. The one I'm thinking of let you submit proofs written in Lean and you'd get a verdict right away, like a competitive programming online judge.

»
13 months ago, hide # |
 
Vote: I like it 0 Vote: I do not like it

wsp i met you at orz

»
13 months ago, hide # |
 
Vote: I like it +13 Vote: I do not like it

Codewars has some

»
13 months ago, hide # |
 
Vote: I like it 0 Vote: I do not like it

This online judge supports checking proofs with Isabelle, Coq/Rocq and Lean: https://do.proof.in.tum.de/competitions/

»
8 months ago, hide # |
← Rev. 2  
Vote: I like it +18 Vote: I do not like it

I know it's an old post but could it be that you are referring to this blog? There is also a more recent follow-up. I am currently working on it, you can check it out at leanoj.org.

  • »
    »
    8 months ago, hide # ^ |
     
    Vote: I like it +3 Vote: I do not like it

    Definitely not the site I originally visited, but it's exactly what I was looking for. I'll try to make some time to log in and submit some problems.

    Keep up the good work!