Designing a user- and machine-friendly theorem prover

Stream: general

[Zhanrong Qiao]

I am in the last year of university at Imperial, and for my final year project (as a maths and CS student) I thought it would be fun to implement a theorem prover using Rust (also, to rethink and finish what I started 3 years ago). I have outlined my current design in the slides; does my reasoning sounds OK, and does it look like something that would work? :smile: this seems so uninformed please ignore it

[Shreyas Srinivas]

1. Why do you want to implement DTT if you want ZFC?
2. Have you looked at epigram?

[Zhanrong Qiao]

1. Finitely axiomatising ZFC requires a second-order logic. Here the basic DTT substitutes that second-order logic, so that I am able to use typed variables (instead of plain sets) in my proofs, with benefits from type inference, operator overloading, etc.
2. Not yet, I will have a look...

[Zhanrong Qiao]

On a second thought, much of this might be implemented as Lean tactics. Are there any attempts or experiments in Lean on maintaining an reusable index of all currently imported definitions (i.e. not restricted to the local context) based on their types in β-normal forms or something?

[Eric Wieser]

Are you aware of loogle and exact??

[Zhanrong Qiao]

Of course, but iirc exact? has to perform a new search each time it is invoked, so you cannot really use it 100+ times in another proof automation procedure and still expect reasonable speed...? Indeed Loogle seems to have an index...

[Shreyas Srinivas]

I recall that the exact?'s predecessor had an index, so it would be surprising if exact? doesn't

[Shreyas Srinivas]

Since you ask for normal forms, there is of course simp?

[Shreyas Srinivas]

Which also indexes all simp lemmas in normal forms

[Jason Rute]

I thought exact? used a discrimination tree for lookup.

[Zhanrong Qiao]

Thank you, I will have a look...

[Kim Morrison]

exact? dynamically builds the discrimination tree on the first call within a given file, but repeated calls should be much faster.

[Shreyas Srinivas]

Btw I don't know how Imperial CS does undergrad projects, but the right person to ask these questions is usually your potential advisor(s). Building a toy ITP with some nifty feature demos might be doable. Making a whole ITP that is usable from scratch can take years. I think lean4 took 3 years and they already had some basic issues sorted out in previous iterations.

[Shreyas Srinivas]

Imperial definitely has a strong PL group

[Shreyas Srinivas]

They should be able to guide you