Skip to content
This repository has been archived by the owner on Oct 14, 2020. It is now read-only.

Coq, HOL-Light, Isabelle/HOL, or Isabelle/ZF #90

Closed
xcthulhu opened this issue Aug 17, 2014 · 2 comments
Closed

Coq, HOL-Light, Isabelle/HOL, or Isabelle/ZF #90

xcthulhu opened this issue Aug 17, 2014 · 2 comments
Labels
request/language

Comments

@xcthulhu
Copy link
Contributor

I've always dreamt that mathematics education, in particular formal proof, could largely be automated.

Codewars could be a platform for this... it could be crazy awesome.
@xcthulhu xcthulhu changed the title Coq, HOL-Light, Isabelle/HOL, Isabelle/ZF Coq, HOL-Light, Isabelle/HOL, or Isabelle/ZF Aug 17, 2014
@kazk kazk mentioned this issue Mar 10, 2017
Closed
@Axure
Copy link

Axure commented Aug 5, 2017

+1
So how is it going?

@kazk kazk mentioned this issue Mar 8, 2019
Closed
@kazk
Copy link
Member

kazk commented Mar 8, 2019

Superseded by #425

@kazk kazk closed this as completed Mar 8, 2019
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
request/language
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@xcthulhu @jhoffner @kazk @Axure