# Zulip Chat Archive

## Stream: general

### Topic: What lean can't do

#### Dean Young (Sep 11 2022 at 21:02):

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 (Sep 11 2022 at 21:09):

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 (Sep 11 2022 at 21:16):

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 (Sep 11 2022 at 21:19):

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 (Sep 11 2022 at 21:19):

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 (Sep 11 2022 at 21:20):

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 (Sep 11 2022 at 21:23):

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 (Sep 11 2022 at 21:23):

(Well, except for `sorry`

axioms I guess. Which means you didn't finish a proof.)

#### Jason Rute (Sep 11 2022 at 21:27):

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

#### Dean Young (Sep 11 2022 at 21:53):

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 (Sep 12 2022 at 01:49):

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 (Sep 12 2022 at 13:11):

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.

Last updated: Dec 20 2023 at 11:08 UTC