Logipedia – Encyclopedia of Formal Proofs | Hacker News Reader

Logipedia – Encyclopedia of Formal Proofs

logipedia.inria.fr

135 pointslelf19 comments

Open articleView on HN

How does this relate to the Archive of Formal Proofs [1] and Mizar's Mathematical Library [2]?

[1] https://www.isa-afp.org/

[2] http://mizar.org/library/

You can also add Coq's to the mix:

[3] https://coq.inria.fr/library/

Each 1-3 is language specific (Isabelle/HOL, Mizar and Coq respectively).

Logipedia too, is using the language Dedukti, although it is designed to translate into other proof languages, and list these on Logipedia.

The systems you mention use a declarative proof approach that's more similar to the way humans might write a math proof, or to the way computer code is written. In contrast, Coq and Lean use "proof scripts" that are more like writing your stuff in a custom macro-assembler that will break as soon as one changes anything in the "script", or even just upgrades to a newer version of the underlying software. Even the resulting proof is basically not readable on its own without re-processing it with the software itself. (Coq used to have a declarative "mathematical proof language", but it was unmantained and they removed it.)

Other systems, e.g. Agda use "proof terms" that are more like a proof that can be read "declaratively", but one where every single step has to be recorded; there's no provision for the system to "fill in" some gaps, unlike with declarative proofs. This can definitely impact readability/surveyability of a development, but the inherent maintainance problems of "proof scripts" do not arise.

I'm not sure what Dedukti is going for from this basic POV. They mention that they're trying to build a general framework that can support multiple logical/proof systems, but the details are not that clear. It's probably going to be a bit clunkier than the systems you mention, particularly at this early stage of development.

I thought Dedukti has a small kernel. Although “small” may be a relative thing (relative to other dependently typed systems.

I've always wanted a 'Wikipedia for formal proofs'. It's never materialised though, sadly.

I would've expected such an online Encyclopedia to form around Coq or Isabelle/HOL, as these languages/assistants seem to be the most popular.

Unfortunately, I've never seen enough momentum behind one proof language to give a wiki a chance of becoming something substantial.

It seems the formal proof community (which is already small) is so spread out over several languages, that it's hard to get the fire burning.

I think a large part of it may be that people are still inventing the languages and we haven't seen enough industry adoption to settle down on a handful of good ones.

We're still in the Cambrian explosion of new ideas and languages.

The best way to get to the future you want is to keep using them and convincing others to join you!

How about a "Rosetta Proof" wiki in the style of "Rosetta Code"? You wouldn't need to settle on one language, and it might help clarify the advantages of one language or another.

Well according to https://deducteam.github.io/ HOL and Coq can be autotranslated to Dedukti (which is the language Logipedia uses)...

> Unfortunately, I've never seen enough momentum behind one proof language to give a wiki a chance of becoming something substantial.

It's probably not far from hoping for the "Wikipedia of programming" where a single programming is used for all programs. There's religious wars on the best approach to everything and even the proof for "1 + 1 = 2" is fundamentally different in different proof assistants.

Because logic as a subject doesn't have a community in itself and a lot of noise instead of signal (can't find anyone who doesn't mention Gödel against science and maths)

Oh very good!

I started a repository for TLA+ modules years ago that I was hoping would turn into something like this [0]. Like many projects I never took it very far but I've been using formal methods in practice for a couple of years now, might be worth revisiting...

[0] https://github.com/agentultra/software-spec-library

what kinds of ways have you been applying TLA? I've been considering whether it's worth learning for practical purposes.

I've used it most often to understand a poorly understood piece of a system that is giving the team a lot of trouble. An example would be a feature that went into development quickly and was iteratively developed in an agile fashion. The senior developer was smart and made some diagrams and accompanying prose to describe the system from a high level. However once the system had been in production for about six months users were discovering and reporting strange behaviors. I wrote some TLA+ models to verify the design and discover the under-specified behaviors.

I've also used it in the design/planning phase of a new project. We started writing models for key features and even hooked TLA+ into our CI pipeline. We planned to also integrate the TLA+ models with quickcheck so that the latter could verify our implementation based on the specification. However that didn't get too far unfortunately.

TLA+ has mostly been useful in helping me understand and solve hard problems where code alone is insufficient as a specification.

There is also Metamath http://us.metamath.org, another wonderful resource. Would be really cool if these two projects could integrate.

Something related to this Logipedia that I'd be interested to see (or work on building one day) is a site intermediate between this and Wikipedia -- a site where users can view or create logical arguments, and combine smaller arguments into larger ones. I'm not sure how many people would actually use such a site, but it'd surely promote a higher level of public discourse than, say, Twitter. The only way we really communicate online is using strings; there has to be some potential for something more structured.

I feel like we need a wiki/wolfram-esque system where knowledge is derived from axioms, propositions, and theorems, all of which can be toggled and shared by users. If you have the flat-earth axiom toggled on, or some set of axioms and propositions that lead to a flat-earth theorem, then you'll see a different entry of knowledge about the earth than I will. We just have to accept that nothing is completely provable in any concrete sense, and people will disagree about the noumenon. Flat-earth is an extreme example, but there are ambiguous parts of our models that you can interpret different ways, and data that can be reasonably argued as (in)valid. I think a unified system of disunity would be more clever than the patchwork of IdeologyPedias we have today. Once sets of truths have been distributed they could be given precedence by a user, with additional optional toggling, and then used/redistributed. I remember seeing an open-source project attempting this, I thought it was called OneModel but my google searches for that name are turning up an unrelated data company. The code seemed pretty gnarly to me at the time, but it's been a couple years since I looked at it.

Edit: changed ridiculous grammar for clarity.

I think we're of a similar mind -- I was imagining a system where a user could input certain premises they agree with or values that they hold, and then they could see what conclusions follow (or would follow, with the addition of further premises). You certainly could end up with dubious conclusions, given what premises you start from. At the very least, though, different ideologies would actually come with an explicit set of premises, and people who disagree with those ideologies would be able to see exactly what they disagree on.

(Not knowledgable about formal proof systems here.)

Does it have something like a "test suite" or a "build status" constantly verifying that the various claimed implications and equivalences are valid, and/or that the translations into other languages are valid?

Since we're mentioning alternatives, there's also http://vdash.org .

Reply on news.ycombinator.com