Stream: Coq users

Topic: Verification of proofs


view this post on Zulip Heime (May 03 2024 at 23:20):

I am aware that coq users have been writing verifications of proofs. I would like to see how they looks like in specific subjects, particularly analysis. Are there any such files around ?

view this post on Zulip Huỳnh Trần Khanh (May 04 2024 at 00:25):

https://github.com/huynhtrankhanh/CoqCP/blob/main/docs/RepeatCompare.md https://github.com/huynhtrankhanh/CoqCP/blob/main/theories/RepeatCompare.v

view this post on Zulip Huỳnh Trần Khanh (May 04 2024 at 00:25):

This is a fun proof that's quite easy to read

view this post on Zulip Li-yao (May 04 2024 at 06:21):

There are many Coq packages under the coq-community organization https://github.com/orgs/coq-community/repositories
corn and coqtail-math might interest you

view this post on Zulip Karl Palmskog (May 04 2024 at 06:43):

the most actively developed library for analysis in Coq these days is likely MathComp Analysis: https://github.com/math-comp/analysis

view this post on Zulip Pierre Courtieu (May 04 2024 at 13:20):

Wait. @Heime what do you call "writing verifications of proofs"? Usually people write "proofs" in coq format, and coq verifies.

view this post on Zulip Heime (May 04 2024 at 17:42):

I mean the files in coq-format that verifies a proof. Would like to see them verify
specific theorems.

view this post on Zulip Karl Palmskog (May 04 2024 at 17:52):

https://madiot.fr/coq100/ - has links to Coq files stating and proving many well-known theorems

view this post on Zulip Heime (May 05 2024 at 01:35):

How would one order them in terms of importance ?

Perhaps like this

  1. MathComp Analysis
  2. Corn
  3. Coqtail Math

Wondering whether verifying a new proof requires coq programming. Does one need to program coq functionality, then call them when devising the proof verification ?

view this post on Zulip Heime (May 05 2024 at 02:41):

@Karl Palmskog Could coqtail-math start having version numbers ?

view this post on Zulip Huỳnh Trần Khanh (May 05 2024 at 04:11):

You don't need to change Coq code at all

view this post on Zulip Huỳnh Trần Khanh (May 05 2024 at 04:13):

BTW when you're learning a new field that's so different from what you're familiar with you should expect your mental model and your preconceptions to be wrong

view this post on Zulip Huỳnh Trần Khanh (May 05 2024 at 04:13):

Like you said "verification of proofs", I don't know what that means and other community members don't either

view this post on Zulip Heime (May 05 2024 at 04:18):

What do you describe the process of proof verification using the coq system ?

view this post on Zulip Mario Carneiro (May 05 2024 at 04:18):

what process are you referring to exactly?

view this post on Zulip Mario Carneiro (May 05 2024 at 04:18):

writing proofs, or running completed proofs?

view this post on Zulip Heime (May 05 2024 at 04:32):

The process of having machine-checked proofs of theorems. What do you call such a process ? In my view there are two aspects

  1. Writing the theorem in some coq format
  2. Writing the commands that machine-checks its proof

view this post on Zulip Mario Carneiro (May 05 2024 at 04:40):

Having proofs isn't a process

view this post on Zulip djao (May 05 2024 at 04:41):

These questions indicate that you haven't even tried the very basics yet. Writing the theorem statements in Coq is more or less identical to what you would write in math using logical symbols. Writing the proofs in Coq is very different since Coq uses a special language ("tactics") for proofs. There is no separate verification process, or at least, there isn't any such process that you need to worry about at this stage. Coq verifies the proofs for you automatically as you go along.

view this post on Zulip djao (May 05 2024 at 04:42):

As you write the proof, Coq verifies it. If the proof does not verify successfully, then you have not written it correctly. You seem to think that writing and verifying proofs are separate processes. They are not, at least, not as far as you're concerned.

view this post on Zulip Heime (May 05 2024 at 04:51):

Yes, quite identical but with text such as "forall" that is specific to coq. Yes. Coq uses tactics which you can run. The tactics provide a proof, not like a proof in a mathematical book, but a proof nonetheless. If I want to verify one of my proofs on a new topic, I might need to write some coq tactics myself, am I right ?

view this post on Zulip djao (May 05 2024 at 04:52):

I never write "forall" in my proofs, I just write ∀, which means the same thing (assuming you have loaded the Utf8 package) but looks more normal to a mathematician.

view this post on Zulip djao (May 05 2024 at 04:52):

Verifying a proof doesn't require you to do anything other than run Coq on your file.

view this post on Zulip djao (May 05 2024 at 04:52):

"coqc file.v" and you're done. This assumes that you've written the proofs in file.v correctly.

view this post on Zulip Heime (May 05 2024 at 04:53):

I can write a proof in terms of tactics, but that does not mean that it verifies successfully.

view this post on Zulip djao (May 05 2024 at 04:53):

Correct, in a way, but I would argue that in that case you haven't written a "proof"

view this post on Zulip djao (May 05 2024 at 04:53):

to write a "proof" means that the proof verifies correctly. Otherwise it is not a proof.

view this post on Zulip Mario Carneiro (May 05 2024 at 04:54):

Put another way, running coq on a coq proof is not fundamentally any different from running gcc on C code

view this post on Zulip djao (May 05 2024 at 04:54):

if your so-called proof does not verify then I would call it a failed attempt at a proof, not a proof

view this post on Zulip Mario Carneiro (May 05 2024 at 04:55):

(in the same way that C code with a syntax or type error isn't really C code)

view this post on Zulip Heime (May 05 2024 at 04:55):

UTF8 is just about rendering, but the actual source code is "forall", is that right ?

view this post on Zulip Mario Carneiro (May 05 2024 at 04:56):

no

view this post on Zulip djao (May 05 2024 at 04:56):

If you want to get started with proofs, I recommend http://michaeldnahas.com/doc/nahas_tutorial -- yes, it is old, and out of date, but so what? It at least focuses on proofs, whereas most other introductory Coq documentation starts with computation.

The actual source code file contains the UTF8 character ∀. The Utf8 package aliases this character to "forall"

view this post on Zulip djao (May 05 2024 at 04:57):

now please, go start working through some tutorials. Asking questions is useless if you don't ever actually use the system.

view this post on Zulip Heime (May 05 2024 at 05:00):

I think of all this differently. You describe a theorem that coq can interpret. You come up with a proof that has not been machine verified yet. You then come up with a new proof that has been machine verified. You might also need to write new constructs and tactics as well before being able to have a verification to succeed.

view this post on Zulip djao (May 05 2024 at 05:02):

It's really obvious that you have never used Coq. What you are describing is perhaps theoretically possible, but completely alien to anyone who uses Coq. We don't use Coq that way!

view this post on Zulip djao (May 05 2024 at 05:05):

What actually happens is: we have a proof. It is not machine verified. We break it down into small steps that we think we can individually achieve on the machine. We then write each small step on the machine, first one step, then the next, then the next, and so on. As we go along, we check what we write. Almost never does it work the first time. We look at what Coq says and then we change our proof, adjust, refine, improve, until that small step succeeds. Then we do the next step. After many hours, days, or weeks, we have a complete proof. It is an interactive, back-and-forth process. There is not a separate concept of proofs and verification. Both go together hand in hand simultaneously.

view this post on Zulip Heime (May 05 2024 at 05:06):

I use emacs, I do write "forall" and not the UTF symbol.

view this post on Zulip djao (May 05 2024 at 05:06):

it doesn't matter really what you write, as long as Coq can read it. The larger point stands. Your mental model is wrong.

view this post on Zulip Heime (May 05 2024 at 05:12):

@djao I understand it as you described. You have a proof you think does work, but then use your computer to be sure each step is successful. If not successful, you make the changes. When the steps succeed, you have the proof that you stick with.

view this post on Zulip Heime (May 05 2024 at 05:16):

Suppose I have some proof for a new wavelet transform technique. Would coq have all the tactics I need ? That's my question.

view this post on Zulip djao (May 05 2024 at 05:17):

You can get very far in Coq without ever needing to write new tactics. If you do encounter a situation where you need to write new tactics, hopefully you are advanced enough in Coq to know how to do that.

view this post on Zulip djao (May 05 2024 at 05:17):

It seems very odd to be asking such questions when you haven't even learned the very basics.

view this post on Zulip Heime (May 05 2024 at 05:25):

If one never wrote new tactics, is there some manual to learn ? Can't one just start straight away - learning coq and learning how to write tactics at the same time ?

view this post on Zulip djao (May 05 2024 at 05:26):

Do you know any programming languages at all? When you're learning C, do you need to write language extensions? Yes, perhaps, at some point, but that point is very far from the beginner level. Start at the beginner level and work your way up from there. It is the same with everything else.

view this post on Zulip djao (May 05 2024 at 05:28):

It's just absolutely bizarre for anyone to be worrying about this at the very start of their journey.

view this post on Zulip djao (May 05 2024 at 05:32):

Some books do cover the tactical language alongside the Coq language, for example http://adam.chlipala.net/cpdt/ (which you should feel free to read); however in my experience these books tend to focus more on computation and software verification than on mathematical proofs.

view this post on Zulip Heime (May 05 2024 at 05:32):

How long does it normally take to use coq without knowing how to write any tactics ? I am unsure whether my work is too advanced for coq to handle. And therefore would need to do more work myself. Do you know if there are any libraries listing proofs involving signal analysis, fourier and wavelet transforms ? Am quite fed up working with toy problems such as arithmetic and logic.

view this post on Zulip djao (May 05 2024 at 05:33):

I really doubt that your problem is tactics. Tactics are never necessary. In theory you can write any proof using lambda calculus proof terms. Almost always the problem is that math itself is hard to formalize.

view this post on Zulip Heime (May 05 2024 at 05:35):

Hard to formalise for a machine to understand ?

view this post on Zulip djao (May 05 2024 at 05:35):

If you are unable to progress beyond simple arithmetic and logic, new tactics are not going to magically allow you to make further progress.

view this post on Zulip djao (May 05 2024 at 05:36):

You have to understand the problem domain much more deeply than you think in order to formalize a proof, tactics or no tactics.

view this post on Zulip Heime (May 05 2024 at 05:37):

I really need to see how people handle proofs from calculus, particularly integral equations.

view this post on Zulip djao (May 05 2024 at 05:38):

You have to train in order to climb the mountain. Yes, there is a risk that no matter how hard you train the mountain will be too hard.
People have already pointed you to many existing libraries containing hundreds if not thousands of examples of proofs. A library is just a collection of proofs. Look inside the source code. Look for the word "Proof."

view this post on Zulip djao (May 05 2024 at 05:39):

https://github.com/math-comp/analysis/blob/master/theories/lebesgue_integral.v Here's another place to start. Dozens of occurrences of "Proof." in that file.

view this post on Zulip Heime (May 05 2024 at 05:41):

There are thousands, but I want to focus on topics that would actually be of use to me.

view this post on Zulip djao (May 05 2024 at 05:41):

The formal proofs community is only a small fraction the size of the larger mathematical community. It is possible, indeed likely, that your specific niche has not been covered yet.

view this post on Zulip djao (May 05 2024 at 05:43):

First you ask simply for examples of proofs (which we have given), and now you want proofs that are of use to you (which we do not have).

view this post on Zulip Heime (May 05 2024 at 05:43):

That's my worry, that it could well be that it has not been covered sufficiently for me yet.

view this post on Zulip djao (May 05 2024 at 05:44):

well, I must admit, I have no interest in wavelets, so you are on your own here. I will say that you have no chance of accomplishing anything with Coq until you start actually using it.

view this post on Zulip djao (May 05 2024 at 05:45):

You cannot learn formal proofs from book reading. You have to DO THE PROOFS. And if the only proofs you do are simple arithmetic and logic proofs, then that is all you will ever be able to do.

view this post on Zulip Heime (May 05 2024 at 05:46):

I asked for examples of proofs in analysis - thinking about special functions and integral equations.

view this post on Zulip djao (May 05 2024 at 05:46):

The entire mathcomp-analysis library is about analysis.

view this post on Zulip djao (May 05 2024 at 05:46):

It might not be your particular brand of analysis, but it is analysis.

view this post on Zulip djao (May 05 2024 at 05:47):

If you insist on only working through examples in your specific niche area, you probably are at a dead end.

view this post on Zulip Heime (May 05 2024 at 05:49):

Fine then. I was curious to know how far people have got on topics close to my area and what to expect in terms of work and effort.

view this post on Zulip Théo Winterhalter (May 05 2024 at 06:16):

It's possible that your topic did not attract the people who might know about your field though. You could try asking in the #math-comp analysis stream about what people think of what you are considering formalising and whether it seems achievable to them.

view this post on Zulip Karl Palmskog (May 05 2024 at 07:51):

Heime said:

Karl Palmskog Could coqtail-math start having version numbers ?

Coqtail does have version numbers, they are based on Coq's version number such as 8.14 and 8.18. See https://github.com/coq/opam/tree/master/released/packages/coq-coqtail

view this post on Zulip Karl Palmskog (May 05 2024 at 07:53):

See also https://github.com/coq-community/awesome-coq and in particular for learning resources: https://github.com/coq-community/awesome-coq?tab=readme-ov-file#books

view this post on Zulip Reynald Affeldt (May 05 2024 at 08:25):

I am not familiar with the topic of integral equations but as a contributor to MathComp-Analysis it looks to me that there are enough special functions and integration theory to at least get started, there are a few papers available online about Lebesgue integration in MathComp-Analysis and these lecture notes that I definitely should be working on https://staff.aist.go.jp/reynald.affeldt/documents/karate-coq.pdf

view this post on Zulip Karl Palmskog (May 05 2024 at 08:28):

@Reynald Affeldt is there any landing website/repository for those lecture notes or is the PDF the canonical reference? (Looks useful to link from Awesome Coq)

view this post on Zulip Reynald Affeldt (May 05 2024 at 08:29):

this is the canonical reference (there was a short homepage for the lecture but the pdf there is not updated)

view this post on Zulip Pierre Courtieu (May 05 2024 at 12:17):

I think the only thing that needs to be said is: coq provide an INTERACTIVE mode (coqtop) that allows to develop the proof interactively. Virtually no one develops coq proofs without it. coqc is basically a silent coqtop which generates .vo files that can then be loaded as libraries by coqtop and coqc.

view this post on Zulip Heime (May 05 2024 at 13:02):

@Reynald Affeldt I was looking to avoid getting started randomly because I could easily waste too much time on things that would be irrelevant to me to think about. For instance, I do not want to delve into mathematical topics to understand the framework before getting to follow a proof.

view this post on Zulip Heime (May 05 2024 at 13:07):

@Pierre Courtieu I agree fully with that assertion. It is quite easy to understand.

view this post on Zulip Heime (May 05 2024 at 13:16):

@Karl Palmskog If I click upon coq-coqtail.8.18, there is no way to download the source.

view this post on Zulip Karl Palmskog (May 05 2024 at 13:19):

https://github.com/coq-community/coqtail-math/releases/tag/8.18 which has this archive: https://github.com/coq-community/coqtail-math/archive/refs/tags/8.18.tar.gz

view this post on Zulip Heime (May 05 2024 at 13:20):

@Karl Palmskog You should include the version number in the readme and not have the users figure out what version is it.

view this post on Zulip Heime (May 05 2024 at 13:26):

So it is coqtail-math rather than coq-coqtail. It is very confusing if one does not clean things up.

view this post on Zulip djao (May 05 2024 at 13:29):

I'm afraid you won't get anywhere with that attitude. Not wanting to delve into mathematical topics is the opposite of what is needed to use a proof assistant.

view this post on Zulip Karl Palmskog (May 05 2024 at 13:32):

coqtail-math is the name of the repository. coq-coqtail is the name of the opam package. The repository has the name coqtail-math to distinguish it from this unrelated project: https://github.com/whonore/Coqtail

Coq uses the opam package manager to distribute code. Version numbers are used primarily for/in opam.

view this post on Zulip Heime (May 05 2024 at 13:34):

From what I understand, some people use UTF8 characters in the actual source code. But then in reality, some UTF package in coq would convert to actual words such as forall. Correct ?

view this post on Zulip djao (May 05 2024 at 13:35):

It's like #define in C.

view this post on Zulip Heime (May 05 2024 at 13:43):

@djao That is how the old school mathematicians used to function. But for some of us, mathematics is not done for mathematical interest or knowledge, but to get some job done. I cannot just pick any topic and simply delve into it for no work benefit.

view this post on Zulip Reynald Affeldt (May 05 2024 at 13:44):

Can you be a bit more precise about your goal?

view this post on Zulip Heime (May 05 2024 at 13:46):

@djao If you open your files with a text editor without UTF capability, do you see forall or an unrecognised glyph ?

view this post on Zulip djao (May 05 2024 at 13:51):

Hard disagree. I use mathematics for a job (cryptography). I could not do this without deep knowledge of the involved mathematics. If you don't need deep knowledge, then you also don't need proofs, and you would have no reason to be here in the first place, since the only purpose of Coq is to provide the proofs.

view this post on Zulip djao (May 05 2024 at 13:52):

A mathematical proof is not needed if you only want to use the mathematics to get a job done and for no other purpose.

view this post on Zulip djao (May 05 2024 at 13:54):

For your UTF8 question, I assure you, the bits in the file are UTF8. I'm not sure what exactly would happen in a "text editor without UTF capability" since opening a UTF8 file in such a text editor would result in undefined behavior.

view this post on Zulip Heime (May 05 2024 at 13:59):

My interests are on topics that have engineering value particularly about signal processing. Thus areas such as Fourier Analysis, Wavelet Decomposition, Special Functions, Functional Analysis, Linear Algebra, Probability. Lot of other mathematical topics are simply disregarded and I put no effort into them (e.g. logic, arithmetic, booleon algebra, geometry, algebraic structures, topology, and so on). And I do not teach, no courses, no anything - just normal work like other people.

view this post on Zulip Karl Palmskog (May 05 2024 at 14:02):

the whole topic about character encoding and meaning of glyphs has been discussed in the literature many times before, see for example http://cs.ru.nl/~freek/pubs/rap.pdf - the short answer is that proof assistants are generally not "safe" against symbol confusion and trickery. But professionals will easily find these issues if serious audits are done.

view this post on Zulip Karl Palmskog (May 05 2024 at 14:04):

see https://math.andrej.com/asset/data/formalizing-invisible-mathematics.pdf#page=16 for the general proof assistant workflow

view this post on Zulip djao (May 05 2024 at 14:06):

I think it is simply not tenable to claim interest in formal proofs while also claiming no interest in logic. This stance is self-contradictory.

view this post on Zulip Heime (May 05 2024 at 14:10):

@djao Right because you require traditional mathematics. I am not in cryptography. We do need to come up with proofs because I work on the development of algorithms. Otherwise an algorithm becomes useless. I also don't care about publication. Our work areas are too far apart.

view this post on Zulip djao (May 05 2024 at 14:10):

It is logically (!) impossible to prove anything without logic.

view this post on Zulip djao (May 05 2024 at 14:11):

I don't care where or what you work on.

view this post on Zulip Heime (May 05 2024 at 14:19):

@djao You should think about it some more. Godel told you about the limits of logic, which many people today fail to comprehend. They heard about it but failed to understand its meaning. David Hilbert was wrong !

view this post on Zulip Heime (May 05 2024 at 14:23):

@djao Stop everything you're doing, and go through the limits of provability in axiomatic theories. The world does not work like that. Ramanujan also knew this but did not need a proof to convince himself.

view this post on Zulip Heime (May 05 2024 at 14:24):

That's why one should bow down to Ramanujan.

view this post on Zulip djao (May 05 2024 at 14:25):

I don't need to convince you of anything. I have given you good advice, if you don't take it then I am done giving advice.

view this post on Zulip Heime (May 05 2024 at 14:36):

I feel like a doctor in an insane asylum where the patients think they are normal and the doctor is crazy. Ramanujan was right, you are wrong.

view this post on Zulip djao (May 05 2024 at 14:37):

Looks like you don't need my advice. That's totally fine.

view this post on Zulip Heime (May 05 2024 at 14:47):

I just do not need to go through many proofs on logic and other toy problems. Just wanted to see the work already done on topics in my area and focus on that so I can extend them. I got some links to specific libraries, which could be helpful. But general discussions are not focused enough for me to entertain.

view this post on Zulip Heime (May 05 2024 at 15:06):

@Karl Palmskog The Yves Bertot article is fantastic. Thank you for that.

view this post on Zulip Heime (May 05 2024 at 15:10):

One thing is for sure. The ANSSI is correct in its statements about accountability - as we at the Gnu Project have been telling the world for decades.

view this post on Zulip Karl Palmskog (May 05 2024 at 15:17):

maybe relevant that we also wrote an article on the Coq Platform, which is the official distribution of Coq together with many plugins and libraries such as MathComp-Analysis

view this post on Zulip Heime (May 05 2024 at 15:35):

@Karl Palmskog Very relevant actually. Of importance is the Coq Test Suite. Are there relatively simple tests categorised by mathematical topic ? Not only for purposes of compatibility, but also as a way for users to use those tests in a way that aids their experience writing and understanding coq proofs and their requirements. Such a test scheme would be of great benefit to everyone. With the added benefit of not requiring so many people asking beginning level questions. Users could then focus more an real problems involving new work instead.

view this post on Zulip Karl Palmskog (May 05 2024 at 15:48):

as partly explained in the paper, there are many "test suites" for Coq.

Then also most serious individual projects use CI based on the official Coq Docker images

view this post on Zulip Karl Palmskog (May 05 2024 at 15:51):

the test-suite is organized by topic, but not necessarily "mathematical domain". The Coq Platform breaks down packages by topic for example here

view this post on Zulip Heime (May 05 2024 at 15:57):

I find the possibility of criticism here particularly on the word "many". This is just a gentle comment about having a basic general mathematics test suite (categorised in a few categorisations in pure and applied mathematics ), not too big or small, and which is customarily unchanging. And with all needed libraries provided.

view this post on Zulip Karl Palmskog (May 05 2024 at 15:57):

it can be argued that MetaCoq is the greatest test devised for Coq itself (a formalization of Coq's calculus and type checking algorithm in Coq itself). However, MetaCoq doesn't currently drive Coq, it's downstream of Coq.

view this post on Zulip Karl Palmskog (May 05 2024 at 16:00):

our general view is that anyone who wants to use Coq for mathematics should start from the Coq Platform, and from there branch out as needed into even more specialized libraries that are available on released part the Coq opam archive (and then possibly further into libraries "in the wild" on GitHub, GitLab, etc.)

view this post on Zulip Gaëtan Gilbert (May 05 2024 at 16:01):

Heime said:

Karl Palmskog Very relevant actually. Of importance is the Coq Test Suite. Are there relatively simple tests categorised by mathematical topic ? Not only for purposes of compatibility, but also as a way for users to use those tests in a way that aids their experience writing and understanding coq proofs and their requirements. Such a test scheme would be of great benefit to everyone. With the added benefit of not requiring so many people asking beginning level questions. Users could then focus more an real problems involving new work instead.

Don't you mean examples? I don't think of tests as being aimed at users.

view this post on Zulip Heime (May 05 2024 at 16:02):

We have had a similar experience with emacs. As the thing got bigger and bigger, and as the old timers vanish, nobody can really figure it in its low level stuff. Big Problem.

view this post on Zulip Heime (May 05 2024 at 16:07):

@Gaëtan Gilbert Ok. Proof examples as a test suite for coq users before going into the wild. And possibly of use to some who may want to go beyond the normal use - so they can get some idea of what could be involved. But the scope must be quite contained for it to work out.

view this post on Zulip Huỳnh Trần Khanh (May 05 2024 at 16:12):

I mean there are people who learned how to use Ltac2 by reading the test suite

view this post on Zulip Karl Palmskog (May 05 2024 at 16:13):

based on my observations, the consensus among Coq developers/researchers is that interactively working through highly organized "book-level" material (such as MCB and Logical Foundations) is the best way for new users to get started. Then there are more specialized tutorials and examples they can work through.

view this post on Zulip Huỳnh Trần Khanh (May 05 2024 at 16:15):

if you study through Software Foundations you might find this UI convenient https://coq.vercel.app/ext/sf/

view this post on Zulip Huỳnh Trần Khanh (May 05 2024 at 16:15):

that's what I used to learn Coq

view this post on Zulip Huỳnh Trần Khanh (May 05 2024 at 16:19):

the most productive thing for you to do right now is just go through Software Foundations and play with the exercises. the equivalent in Lean is the Natural Number Game

view this post on Zulip Huỳnh Trần Khanh (May 05 2024 at 16:20):

after going through introductory material you'll be better informed and can pose better questions

view this post on Zulip Heime (May 05 2024 at 16:20):

Think about this. If the Coq Platform could go a bit further and provide a specific example suite that people can use whose scope is not so basic. In this way, the transition towards specialised libraries and possibly further could became softer. This means that people could stay working with the Coq Platform tools a bit longer whilst getting their skills sharper. I am quite sure that the Coq Platform is better suited for this, because other libraries could have a diverse set of priorities which cannot be completely relied upon without getting unnecessarily confused at the start of the journey.

view this post on Zulip Huỳnh Trần Khanh (May 05 2024 at 16:21):

at the end of the day the math is hard :( I don't think there's much the Coq Platform can do

view this post on Zulip Huỳnh Trần Khanh (May 05 2024 at 16:22):

I feel the primary bottleneck is having the right proof strategy, the technical details of dealing with Coq are not as hard

view this post on Zulip Heime (May 05 2024 at 16:24):

If I am able to progress enough to my satisfaction, perhaps I could provide some useful things to make the process joyful.

view this post on Zulip Huỳnh Trần Khanh (May 05 2024 at 16:26):

I feel it's too early for you to talk about this

view this post on Zulip Huỳnh Trần Khanh (May 05 2024 at 16:26):

learn the basics first :)

view this post on Zulip Karl Palmskog (May 05 2024 at 16:27):

we have discussed having "Platform tutorials" that show different combinations of techniques available through Platform packages. However, I think it's essentially niche content at this point, since most people get stuck earlier on more "trivial" things, such as UI and grappling with tactics and the specification language (Gallina)

view this post on Zulip Heime (May 05 2024 at 17:04):

@Karl Palmskog I see. Hopefully it will progress and become a useful and established way once the earlier blocks stop being a problem in future. From your description, generally people need to go through extremely simple proofs, otherwise they immediately get stuck.

view this post on Zulip Heime (May 05 2024 at 17:18):

Could be a long road till all this becomes mainstream. And I want to help as I find such an endeavor meaningful. To me at least. But to convince others - quite hard. Even harder to have them help me.

view this post on Zulip Karl Palmskog (May 05 2024 at 17:22):

well, you usually need to go through very simple proofs to know what to do to get unstuck. The classic case is someone trying to formalize a pen-and-paper proof and failing deep inside the Coq proof attempt due to some small fact that should be obvious not holding.

view this post on Zulip Karl Palmskog (May 05 2024 at 17:25):

if you are using some highly automated tactics, you then drop to more elementary tactics and find the smallest possible step where you fail, and that's typically where the missing piece becomes obvious

view this post on Zulip Karl Palmskog (May 05 2024 at 17:28):

but more generally, just making the statement to prove in the "right" form can be very challenging. And if you state it in the wrong form, the difficulty of formal proof can increase several orders (e.g., take an order of magnitude longer to complete, minutes vs. days)

view this post on Zulip Karl Palmskog (May 05 2024 at 17:33):

When I looked at it in more detail in 2019, proof assistant user productivity was not addressed in any serious way (compared to software developer productivity) in the literature (p. 214 in https://arxiv.org/abs/2003.06458)

view this post on Zulip Heime (May 05 2024 at 17:43):

I come from the industrial mathematics software engineering productivity. So at this point quite critical of the typical university mathematician. I find that they do a lot of mistakes and they get angry as they feel better than they actually are. Of course, they can be quite capable if they put their mind to it.

view this post on Zulip Heime (May 05 2024 at 17:46):

@Karl Palmskog I noticed that. The problems involved in getting to the "right form" required.

view this post on Zulip Karl Palmskog (May 05 2024 at 17:48):

Heime said:

I come from the industrial mathematics software engineering productivity. So at this point quite critical of the typical university mathematician. I find that they do a lot of mistakes and they get angry as they feel better than they actually are. Of course, they can be quite capable if they put their mind to it.

Kevin Buzzard highlighted an example where the same math journal to this day has papers published that directly contradict each other, and you have to get access to a paywalled math paper review site to know which one is correct (slide 6-7 in https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_buzzard.pdf)

view this post on Zulip Heime (May 05 2024 at 17:59):

Yes, I have talked to Kevin. I also have found many mistakes in publications - but few have talked about it. I have now stopped reviewing to concentrate on my own work only. Rather than read papers, it is more productive to work directly with others without spending time on peer-review publishing.

view this post on Zulip Heime (May 05 2024 at 18:03):

Today, I give this advice - if you have to get access to a paywalled math paper to know which one is correct, don't bother with it. Work on topics you can do without using paywalled papers, but work directly with the individuals involved. The current evolution of the university system will became extinct - it has no value even today.

view this post on Zulip Karl Palmskog (May 05 2024 at 18:07):

as of right now, there are still very few employment opportunities outside academia to work with any of Coq, Lean, Isabelle, etc. (at least consistently)

view this post on Zulip Heime (May 05 2024 at 18:10):

It is my wish and my blessing for more opportunities for the energetic young ones. I am one of the old sods from the early 80's. You have the power today to go beyond our bull.

view this post on Zulip Huỳnh Trần Khanh (May 06 2024 at 00:22):

the free market is my ultimate judge :)

view this post on Zulip Huỳnh Trần Khanh (May 06 2024 at 00:23):

I don't want to be in academia. I feel formal verification has a lot of potential in the brutal free market

view this post on Zulip Heime (May 06 2024 at 12:33):

It is the future. I am all for free enterprise myself. Do what is important to you, the result is not up to you.


Last updated: Jun 13 2024 at 21:01 UTC