Array.anyM is inconsistent

Stream: lean4

[Jun Yoshida]

The bound-check of Array.anyMUnsafe and Array.anyM are inconsistent. As a result, we have

theorem any_t : #[true].any id 0 2 = true := by
  decide

theorem any_f : #[true].any id 0 2 = false := by
  native_decide

which together imply False.

The bug seems to have already been filed in lean4#1921 about 10 months ago. Any problem? @Mario Carneiro @Gabriel Ebner

[Scott Morrison]

(For the sake of any innocent bystanders, note that #print axioms any_f includes Lean.ofReduceBool, which tells you that you've taken the guard-rails off and are calculating rather than proving.)

[Ioannis Konstantoulas]

Scott Morrison said:

(For the sake of any innocent bystanders, note that #print axioms any_f includes Lean.ofReduceBool, which tells you that you've taken the guard-rails off and are calculating rather than proving.)

To emphasize, the documentation warns of the danger appropriately loudly: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Lean.ofReduceBool

[Eric Rodriguez]

Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.

This reads to me as 'we're fairly sure it's correct but we're not sure', not 'you can definitely prove False'

[Scott Morrison]

lean4#2641 fixes lean4#1921, using Mario's suggestion.

[Jun Yoshida]

Thank you @Scott Morrison. Maybe I could make that PR, but I just wanted to know why the fix was not created beforehand.

[Scott Morrison]

Just that no one had the time, I think.

[Jun Yoshida]

I thought so. Sorry for bothering you all.

[Scott Morrison]

Not at all! Your post prompted me to do it.

[Martin Dvořák]

You forgot to write the most important corollary!

import Mathlib.Tactic

theorem FLT (a b c n : ℕ) :
  (0 < a) → (0 < b) → (0 < c) → (2 < n) →
    a ^ n + b ^ n ≠ c ^ n := by
  intros
  have abracadabra : #[true].any id 0 2 = false
  · native_decide
  simp at abracadabra
  done

:tada: :tada: :tada:

[Mac Malone]

Eric Rodriguez said:

This reads to me as 'we're fairly sure it's correct but we're not sure', not 'you can definitely prove False'

It is ideally correct insofar as the code you are using is expected to be implemented correctly (thus anyM was a bug that needing fixing). However, in general, it is easy to forcefully derive a False from native_decide on arbitrary user code. For example:

def one := 1
@[implemented_by one] def zero := 0
theorem zero_ne_eq_one : False := by
  have : zero ≠ one := by decide
  have : zero = one := by native_decide
  contradiction
#print axioms zero_ne_eq_one
 -- zero_ne_eq_one' depends on axioms: [Lean.ofReduceBool]

[Mac Malone]

Thus, proofs using depending on native_decide and its axiom (i.e., ofReduceBool) from untrusted users can be suspect.

[Mario Carneiro]

I have on the todo list a mechanism to collect up the implemented_by and extern declarations used by a lean function, which should help address this issue

[Jun Yoshida]

Does that mean uses of Array are to be deprecated in theorem proving scene?

[Mac Malone]

@Jun Yoshida I am not sure quite what you are referring too, but it is certainly possible to prove things about Array soundly without using native_decide (that is what the reference implementations are designed to enable).

[Jun Yoshida]

Yes, but a lot of basic functions on Array, including the constructor Array.mk, have implemented_by attributes. The arguments above seem to imply that it is hard to think of such functions as a part of trusted codebase.

[Tomas Skrivan]

Using arrays in proofs without native_decide is just using List with a slightly different API.

[Mac Malone]

As @Tomas Skrivan notes, implemented_by is only really an issue in the context of native_decide. Without it, one is just dealing with the Lean Expr view of the Array, which is just a wrapper around a List. implemented_by does not impact this level (implemented_by is for codegen).

[Jun Yoshida]

Ah, that's right. Thank you for pointing it out.

[Ioannis Konstantoulas]

I am confused; if a mathematician (non-programmer) asks me if arrays are ok in their proofs, what should I tell them? More importantly, what if they don't ask me?

[Eric Wieser]

The answer is that native_decide is placing trust in a lot more things (as it says in the documentation), and one of those things is that every implemented_by attribute is correct (in the sense that the functions really coincide everywhere).

[Eric Wieser]

There is no reason to single out Array, as demonstrated by Mac's post above which doesn't mention it

[Ioannis Konstantoulas]

My example is meant to demonstrate the level of question a non-lean expert would ask, and the kind of concern they would display. The answer you give @Eric Wieser is completely opaque to them: what depends, directly or indirectly, on native_decide? Is that " native_decide" a unique thing we need to keep in mind when writing proofs, or are there other things that compromise soundness? How do we know?

[Eric Rodriguez]

I think the key thing is to have Mario's tool, because then you can inspect your trusted code base.

[Eric Wieser]

If you care only about mathematics, then you probably want to completely avoid native_decide (as it pulls in the docs#Lean.ofReduceBool axiom)

[Eric Wieser]

In general if you want to know whether you can trust a proof, use #print axioms. If it prints anything other than choice, propext, Quot.sound, then you have to think very carefully about whether you trust the extra things in the list.

[Ioannis Konstantoulas]

In light of the recent thread, I sadly see we need to be more careful than relying on #print axioms.

[Eric Wieser]

I think in a previous thread we saw that #print axioms is not foolproof against a malicious attacker; but I think it is in combination with leanchecker

[Ioannis Konstantoulas]

Nice; Scott just corrected a concern I had about leanchecker. I think when leanchecker is completely ready, we should emphasize its existence and role to mathematicians.

[Patrick Massot]

Ioannis Konstantoulas said:

I think when leanchecker is completely ready, we should emphasize its existence and role to mathematicians.

I strongly disagree with this. All this discussion is completely irrelevant to mathematics. This recent obsession comes purely from the new software engineering and computer science side of the community and is only noise from the mathematical point of view. All those issues simply do not arise on the mathematics side. I know you are also interested in mathematics, but "porting shell scripts" is not part of mathematics.

[Patrick Massot]

Ioannis Konstantoulas said:

if a mathematician (non-programmer) asks me if arrays are ok in their proofs

How would that happen?? How would they meet arrays?

[Ioannis Konstantoulas]

This confuses me so much! Isn't leanchecker supposed to be the thing that verifies the veracity of proofs?? What the hell am I missing now!

Never mind, I am a little too angry now to talk.

[Henrik Böving]

Ioannis Konstantoulas said:

This confuses me so much! Isn't leanchecker supposed to be the thing that verifies the veracity of proofs?? What the hell am I missing now!

Never mind, I am a little too angry now to talk.

Yes it is but the point is that the mathematicians trust code they write themselves + code that is already in mathlib and accepted both by the maintainers and the compiler enough that this "cheat the system" type of stuff is a non issue from their POV

[Damiano Testa]

Speaking for myself, the biggest added value of formalization for me is not verifying maths. I am not at all worried that some theorem that I thought was true is in fact false.

For me, one of the biggest reasons for being interested in formalization is actually digitalisation, pattern finding and automation.

[Kevin Buzzard]

Unlike the computer scientists we have no interest in hacking the system. We are trying to build a beautiful library of our beliefs. We're not checking our work -- this is a big misconception that some people have. We're just storing it.

[Ming Li]

Could you tell more about the mission of such a library? How will it be used in the future?

[Scott Morrison]

I have to admit I agree with Patrick's rather extreme position here. :-)

lean4checker is of course helpful if you want machine verified proofs, and for some reason have decided to trust the Lean kernel but very little else.

But generally I think it is a terrible idea if we advertise to mathematicians that the point of Lean is that the computer will verify your proofs. That would be rather unappealing, and I think besides the point!

The reason mathematicians should use Lean are:

• it's fun
• it brings mathematics and programming closer, as they always ought to have been
• the computer can (one day, hopefully, :fingers_crossed:) actually help you do mathematics
• we're building a big coherent library that will enable other interesting things
• we sometimes learn interesting things from formalisation (if only how to Bourbaki a topic)
• ... and the big one: Lean + Mathlib + ML might be the playground where AGI grows up, and that will be fun to watch. :-)

[Kayla Thomas]

I'm not intending to make any argument about the discussion, but as a rather amateur mathematician, having the computer check my proofs is one of the big appeals of Lean to me. It means I don't have to keep asking someone if my handwritten proof is correct when I am trying to learn mathematics.

[Chris Wong]

I learned about filters and hypermaps from formalization. So +1 to that point!