New online seminar series: Every proof assistant

[FredJeffries]

Andrej Bauer has announce a "series of seminars titled 'Every proof assistant' that would be devoted to all the different proof assistants out there."

http://math.andrej.com/2020/04/28/every-theorem-prover/

[Mostowski Collapse]

First "Every proof assistant" seminar:

Arend proof assistant
Time: Thursday, April 30, 2020 from 18:00 to 19:00
(Central European Summer Time, UTC+2)
Location: online at Zoom ID 965 4439 5816
Speaker: Valery Isaev (JetBrains research)


Didn't know that IntelliJ folks are working
on a theorem prover called Arend (Heyting).

https://de.wikipedia.org/wiki/Arend_Heyting

[Ross A. Finlayson]

There are lots of routine software generation and
maintenance tasks that make for simple, effective
reasoning about program artifacts and logic validation,
that it's an abstraction itself of the syntax, the
theorem-proving in usually deterministic models of
defined behavior in usual computational settings.

Software purposing and generation from schema is
so usual that term-rewriting systems and so on
pretty much make "logic" and the artifact fungible
(tractable).

https://en.wikipedia.org/wiki/Stratego/XT

Model-based software engineering has that there are
lots of lessons in formal automata usually un-learned
by usual coders given an entry point and I/O's
(and a miniature specification).

Discovering and extracting de facto models is
"a" and sometimes "the" usual exercise in coding
more-than-less "standard" logic of automata.

[Mostowski Collapse]

Possibly HoTT people are less intersted in
computer science applications, more in analysis
applications:

"The 20th century saw the development of ZFC
set theory, which today is the standard foundation
of mathematics."

"HoTT is an alternative foundation that is based
on integrating concepts from topology into a
typed logic which avoids the need for ZFC set
theory and its troublesome axioms."

The Arend proof assistant tries to do
something with HoTT: "Arend implements a version of
homotopy type theory with an interval type, which
syntax is similar to cubical type theory."

[Mostowski Collapse]

BTW: First video is out, but did not
yet have time to watch it in full:

Valery Isaev: Arend proof assistant
https://vimeo.com/413726748

[Mostowski Collapse]

They are marching on:

MMT – A FOUNDATION-INDEPENDENT LOGICAL SYSTEM
Florian Rabe (University of Erlangen)
https://vimeo.com/421123419

Planned:

May 28, 2020: Brigitte Pientka - Beluga
June 4, 2020: Jon Sterling - redtt (to be confirmed)
June 11, 2020: Conor McBride - Epigram 2
June 25, 2020: William J. Bowman, Cur
July 2, 2020: Anders Mörtberg - Cubical Agda

Am Donnerstag, 30. April 2020 00:14:43 UTC+2 schrieb FredJeffries:

[Me]

On Tuesday, May 26, 2020 at 1:56:16 AM UTC+2, Mostowski Collapse wrote:

> MMT – A FOUNDATION-INDEPENDENT LOGICAL SYSTEM
> Florian Rabe (University of Erlangen)
> https://vimeo.com/421123419

It's a small world. Following some advice concerning JG's nonsensical "limit definition" I found the following analysis:

Math Crankery with John Gabriel – “Cauchy’s Kludge”
http://blog.logicalphalluses.net/2017/03/04/math-crankery-with-john-gabriel-cauchys-kludge/

There I stumbled over the paragraph:

"I love how he calls the limit definition “ill-defined” and then gives an (apart from the error above) rigorous, formal definition in first-order logic. Seriously, you can’t make something more well-defined than by using first-order logic. I mean, that’s kind-of what first-order logic is for! You can even input this definition in an automated theorem prover and see that it checks out. Just for fun, I did exactly that in our own MMT system"

MMT system =>

http://blog.logicalphalluses.net/2016/08/20/meta-meta-tools-and-theory-graphs-what-is-mmt/

:-)

[Mostowski Collapse]

Cranks are always fun. Like Dan-O-Matik, who
thinks that he can prove Zorn's Lemma from nothing.
Not to mention some bats scattering space.

[Mostowski Collapse]

Possibly the best Proof Assistant would be
a Proof Assistant that could reason about
its own tactics. Making tactics less ad-hoc.

This could require to have a tactics language
that is amenable to proofs it self. Like
first proving cut elimination correct, and

then using cut elimination. Anyway what are
tactics, here a first intro:

How do 'tactics' work in proof assistants?
https://cstheory.stackexchange.com/questions/5696/how-do-tactics-work-in-proof-assistants

[Mostowski Collapse]

New Video out:

Jon Sterling (Carnegie Mellon University)
Abstract: redtt is an interactive proof assistant
for Cartesian cubical type theory, a version of
Martin-Löf type theory featuring computational
versions of function extensionality, higher
inductive types, and univalence.
https://vimeo.com/425917591