The Coq mailing list

[Kevin Buzzard <kevin.m.buzzard AT gmail.com>]

On Wed, 4 Mar 2020 at 07:18, Martin Escardo <m.escardo AT cs.bham.ac.uk> wrote:

Dependent types are good for pure mathematics (classical or
constructive). They are the natural home to define group, ring, metric
space, topological space, poset, lattice, category, etc, and study them.
Mathematicians that use(d) dependent types include Voevodsky (in Coq)
and Kevin Buzzard (in Lean), among others. Kevin and his team defined,
in particular, perfectoid spaces in dependent type theory. Martin

The BCM (Buzzard, Commelin, Massot) paper defined perfectoid spaces in Lean

and looking forwards (in the sense of trying to attract "working mathematicians"

into the area of formalisation) I think it's an interesting question as to whether this definition

could be made in other systems in a way which is actually usable. My guess: I don't see why it couldn't

be done in Coq (but of course the type theories of Lean and Coq are similar), although

there is a whole bunch of noncomputable stuff embedded in the mathematics.

I *suspect* that it would be a real struggle to do it in any of the HOL systems

because a sheaf is a dependent type, but these HOL people are good at tricks

for working around these things -- personally I would start with seeing whether

one can set up a theory of sheaves of modules on a locally ringed space in a HOL

system, because that will be the first stumbling block. And as for the HoTT systems,

I have no feeling as to whether it is possible to do any serious mathematics other than

category theory and synthetic homotopy theory -- my perception is that

the user base are more interested in other kinds of questions.

In particular, connecting back to the original question, a sheaf of modules on a

locally-ringed space is a fundamental concept which shows up in a typical MSc

or early PhD level algebraic geometry course (they were in the MSc algebraic

geometry course I took), and if one wants to do this kind of mathematics in a

theorem prover (and I do, as do several other people in the Lean community)

then I *suspect* that it would be hard without dependent types. On the other hand

I would love to be proved wrong.

Kevin

On 03/03/2020 19:43, jasongross9 AT gmail.com wrote:
> I'm in the process of writing my thesis on proof assistant performance
> bottlenecks (with a focus on Coq), and there's a large class of
> performance bottlenecks that come from (mis)using the power of dependent
> types.  So in writing the introduction, I want to provide some
> justification for the design decision of using dependent types, rather
> than, say, set theory or classical logic (as in, e.g., Isabelle/HOL). 
> And the only reasons I can come up with are "it's fun" and "lots of
> people do it"
>
> So I'm asking these mailing lists: why do we base proof assistants on
> dependent type theory?  What are the trade-offs involved?
> I'm interested both in explanations and arguments given on list, as well
> as in references to papers that discuss these sorts of choices.
>
> Thanks,
> Jason
>
> _______________________________________________
> Agda mailing list
> Agda AT lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe