I recently did some work using the new Lean Prover, proving group theory
theorems up to the First Sylow Theorem
(https://github.com/htzh/leanproved). What is impressive about the
dependent type based ITP is the type feedback it gives to the user. Proving
a theorem is very much like talking to a compiler, convincing it that
certain operations are correct and safe. Lean’s library currently focuses
on mathematics. Coq does have code extraction but I think the extracted
code is not necessarily optimal. I wonder what it would take to integrate
ITP type of capability into ATS, so that users can get more useful feedback
and provide guidance for solving constraints that can not be automatically
solved.
Lean’s code base is in C++, and is quite lean (no pun intended) with a
liberal license. The main architect Leo Demoura is also the creator of Z3.
There could be some interesting synergy if ATS can somehow take advantage
of Lean (http://leanprover.github.io/). At a minimum Lean’s Emacs based IDE
works great and can be a useful framework for projects with similar needs.
It is certainly quite impressive, to say the least.
However, I do not feel, at least for now, that having more ITP support in
ATS is the “right” way
to go. Instead, I would suggest more research into ATP (automated TP). For
instance, studying
how constraints gather during ATS-typechecking can be solved using Z3. To
do a good job, you
need to know a lot about the kind of quantifer-elimination “magic” in Z3.
As far as IDE is of the concern, we have to wait for the person/people who
has/have both the
skills and the urge to do it To me, one essence here is to have
extensive support for meta-programming
in the IDE.On Wednesday, September 9, 2015 at 2:46:28 PM UTC-4, H Zhang wrote:
I recently did some work using the new Lean Prover, proving group theory
theorems up to the First Sylow Theorem (GitHub - htzh/leanproved: Theorems proved using the Lean prover.).
What is impressive about the dependent type based ITP is the type feedback
it gives to the user. Proving a theorem is very much like talking to a
compiler, convincing it that certain operations are correct and safe.
Lean’s library currently focuses on mathematics. Coq does have code
extraction but I think the extracted code is not necessarily optimal. I
wonder what it would take to integrate ITP type of capability into ATS, so
that users can get more useful feedback and provide guidance for solving
constraints that can not be automatically solved.
Lean’s code base is in C++, and is quite lean (no pun intended) with a
liberal license. The main architect Leo Demoura is also the creator of Z3.
There could be some interesting synergy if ATS can somehow take advantage
of Lean (http://leanprover.github.io/). At a minimum Lean’s Emacs based
IDE works great and can be a useful framework for projects with similar
needs.
HaitaoOn Wednesday, September 9, 2015 at 11:46:28 AM UTC-7, H Zhang wrote:
I recently did some work using the new Lean Prover, proving group theory
theorems up to the First Sylow Theorem (GitHub - htzh/leanproved: Theorems proved using the Lean prover.).
What is impressive about the dependent type based ITP is the type feedback
it gives to the user. Proving a theorem is very much like talking to a
compiler, convincing it that certain operations are correct and safe.
Lean’s library currently focuses on mathematics. Coq does have code
extraction but I think the extracted code is not necessarily optimal. I
wonder what it would take to integrate ITP type of capability into ATS, so
that users can get more useful feedback and provide guidance for solving
constraints that can not be automatically solved.
Lean’s code base is in C++, and is quite lean (no pun intended) with a
liberal license. The main architect Leo Demoura is also the creator of Z3.
There could be some interesting synergy if ATS can somehow take advantage
of Lean (http://leanprover.github.io/). At a minimum Lean’s Emacs based
IDE works great and can be a useful framework for projects with similar
needs.
I agree that ATP would be nice. Certainly the many arithmetic
(associativity, commutativity etc) and logic lemmas ( A and B → A, e.g.)
should be automated so that users don’t have to memorize the names. This
would improve efficiency and user experience. I think Leo is working on a
simplifier for Lean. It will be interesting to see how that works out.
ITP and meta-programming are both about talking to the compiler (type
checker) so my hope is that the techniques developed for ITP can be used to
assist meta-programming.
HaitaoOn Sunday, September 13, 2015 at 2:18:13 PM UTC-7, gmhwxi wrote:
I took a look at Lean’s Emacs-based IDE.
It is certainly quite impressive, to say the least.
However, I do not feel, at least for now, that having more ITP support in
ATS is the “right” way
to go. Instead, I would suggest more research into ATP (automated TP). For
instance, studying
how constraints gather during ATS-typechecking can be solved using Z3. To
do a good job, you
need to know a lot about the kind of quantifer-elimination “magic” in Z3.
As far as IDE is of the concern, we have to wait for the person/people who
has/have both the
skills and the urge to do it To me, one essence here is to have
extensive support for meta-programming
in the IDE.
On Wednesday, September 9, 2015 at 2:46:28 PM UTC-4, H Zhang wrote:
I recently did some work using the new Lean Prover, proving group theory
theorems up to the First Sylow Theorem ( GitHub - htzh/leanproved: Theorems proved using the Lean prover.). What is impressive about the
dependent type based ITP is the type feedback it gives to the user. Proving
a theorem is very much like talking to a compiler, convincing it that
certain operations are correct and safe. Lean’s library currently focuses
on mathematics. Coq does have code extraction but I think the extracted
code is not necessarily optimal. I wonder what it would take to integrate
ITP type of capability into ATS, so that users can get more useful feedback
and provide guidance for solving constraints that can not be automatically
solved.
Lean’s code base is in C++, and is quite lean (no pun intended) with a
liberal license. The main architect Leo Demoura is also the creator of Z3.
There could be some interesting synergy if ATS can somehow take advantage
of Lean (http://leanprover.github.io/). At a minimum Lean’s Emacs based
IDE works great and can be a useful framework for projects with similar
needs.
To me, one essence here is to have