What lean can't do

Stream: general

[Dean Young]

Beginner's question: suppose I obtain in lean a proposition roughly involving nat, C, R, Z, Type, and Prop. Does the design of Lean ensure that this proposition is correct? Is it true by the design of lean that no axioms were added in which would effect equations in C, R, Z, etc.?

[Henrik Böving]

I'm not quite sure what you are asking here:

• If you obtain a proof of a proposition it is (assuming that the type theory and kernel of Lean does not have inconsistencies which as far as we know it does not) guaranteed that your proof is correct
• You can add axioms to the Lean system yourself via the axiom command in which case the consistency of the system can of course not be guaranteed anymore but as long as your axiom is sound with respect to the rest of the system everything should be fine still

[Yakov Pechersky]

A clarification of language, Dean, what do you mean you obtain a proposition? And by correct? Do you mean obtain a proof of a proposition? Because I can do the following

#check 1 = 2
#check let h : Prop := 1 = 2 in h

and there, I have "obtained" propositions in lean that are well formed expressions. But I have no proof of them.

[Yakov Pechersky]

If I assume a false proposition, I can prove anything to be true! And false propositions do not list in the axioms used:

lemma foo (h : 1 = 2) : 3 = 4 :=
absurd h dec_trivial

#print axioms foo
/-
no axioms
-/

[Jason Rute]

To be clear about axioms, Lean has classical axioms like choice in its core library and they could easily be added to your proof depending on the tactics and theorems you use in your proof. You can check however for what axioms are used in a theorem with #print axioms mythm. [Edit: Missed that Yakov just said this. :face_palm: ]

[Yakov Pechersky]

However, if I used an axiom or sorry in proving some statement, then it will list:

lemma this_is_not_true : 1 = 2 := by sorry

lemma bar : 3 = 4 :=
absurd this_is_not_true dec_trivial

#print axioms bar
/-
[sorry]
no axioms
-/

[Jason Rute]

But it should be pointed out that all of Lean's axioms are consistent with each other, so you won't get a contradiction from incompatible axioms.

[Jason Rute]

(Well, except for sorry axioms I guess. Which means you didn't finish a proof.)

[Jason Rute]

Maybe it would help to explain @Dean Young what you are afraid of going wrong if this doesn't answer your question.

[Dean Young]

Jason Rute said:

Maybe it would help to explain Dean Young what you are afraid of going wrong if this doesn't answer your question.

Your response was very helpful, thanks so much!

At first I wanted to make sure that my definitions have a "dictionary" with mathlib's definitions when they overlap. That way my library can be more mainstream and more people will benefit from it. I wanted to make sure that when I prove something with this library, there's always the option of translating back to the original definitions in mathlib.

After some thought, I think it is more a matter of the definitions meaning what they say. And so now I know what my real goal is to make a dictionary.

[Mario Carneiro]

After some thought, I think it is more a matter of the definitions meaning what they say. And so now I know what my real goal is to make a dictionary.

Of course lean can't prevent you from defining rat and calling it real or anything like that. Only a human (or, if you insist, an ML trained on human math) can actually check that definitions are really what they are supposed to be. But because mathlib is a human-curated artifact, I think there is very low chance of something being totally mislabeled in mathlib, although sometimes it makes minor modifications as part of adapting to type theory and/or formalization, and sometimes the literature itself is split on where to assign certain names

[Dean Young]

Thanks all for your help. I have a much better understanding now.

I'm still getting used to using the site, so I didn't see your replies at first.