## Stream: general

#### Cameron Crossman (Dec 11 2018 at 20:34):

theorem barber_paradox : ¬ (∀ x : men, shaves barber x ↔ ¬ shaves x x)

#### Andrew Ashworth (Dec 11 2018 at 20:37):

Do you have a specific question?

#### Chris Hughes (Dec 11 2018 at 20:44):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Logic.20.26.20Proof

#### Abhimanyu Pallavi Sudhir (Dec 16 2018 at 14:51):

theorem barber_paradox : ¬ (∀ x : men, shaves barber x ↔ ¬ shaves x x)

See barber_is_dead (and a tactic mode proof above it) here: https://github.com/abhimanyupallavisudhir/lean/blob/master/logic_theorems.lean

#### Kevin Buzzard (Dec 16 2018 at 15:07):

Ha ha are you revising Cantor's theorem :-)

#### Kevin Buzzard (Dec 16 2018 at 15:10):

I don't think you need to be classical for pants on fire. I had to prove this in cantor at the end

#### Kevin Buzzard (Dec 16 2018 at 16:48):

example (P : Prop) (Q : Prop) : ¬ P → (P → Q) := by intros;contradiction etc. Your instinct as a mathematician is to case split, but it's often not necessary. Not that this matters (at least not that it matters to us mathematicians...)

#### Norbert Bátfai (Aug 14 2020 at 10:54):

I am enthusiastic because I have recently read Kevin Buzzard’s article: When will computers prove theorems? I really liked the comparison of LaTeX and Lean from the point of view of the progress of mathematics. Now I have already started to get acquainted with the language of Lean. I am working on an informatically-philosophically inspired manuscript in which I would like to put a Lean proof. I chose the Barber Paradox. Partly based on the conversations here, I have made a proof and would like to ask that is it correct?

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber ( h : ∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y )
: false :=
exists.elim h
( assume barber,
begin
intro h,
have hbarbermpr : ¬shaves barber barber → shaves barber barber,
from iff.mpr (h barber),
have hbarbermp  : shaves barber barber → ¬shaves barber barber,
from iff.mp (h barber),
have nsbb : ¬shaves barber barber, from
assume sbb : shaves barber barber,
show false, from hbarbermp sbb sbb,
show false, from nsbb (hbarbermpr nsbb)
end
)
#print NoSuchBarber


#### Kenny Lau (Aug 14 2020 at 10:57):

Norbert Bátfai said:

is it correct?

The whole point of Lean is that you can ask Lean if it's correct. If there are no errors, then it's correct.

#### Kyle Miller (Aug 14 2020 at 10:57):

(assuming you formalized the statement correctly)

#### Eric Wieser (Aug 14 2020 at 11:27):

Could save two lines in your manuscript with:

have hbarber : ¬shaves barber barber ↔ shaves barber barber,
from h barber,


and then use hbarber.mpr instead of hbarbermpr below

#### Scott Morrison (Aug 14 2020 at 11:28):

well, you could save more than that :-)

Oh, for sure :)

#### Chris Wong (Aug 14 2020 at 12:21):

I guess it comes down to context. If the purpose of the code snippet is to demonstrate Lean to a lay audience, then having all the intermediate steps spelled out can be helpful. But someone writing for mathlib – whose audience is experienced Lean programmers – would use a much terser style.

#### Kevin Buzzard (Aug 14 2020 at 12:22):

import tactic

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber ( h : ∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y )
: false :=
exists.elim h
( assume barber,
begin
intro h2, -- I don't want two hypotheses called h
have hbarber := h2 barber, -- human-generated good idea
tauto!, -- computer can finish it off
end
)


#### Kevin Buzzard (Aug 14 2020 at 12:23):

but of course this teaches you far less :-)

#### Norbert Bátfai (Aug 14 2020 at 12:23):

Thanks, so the proof is really nicer:

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber ( h : ∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y )
: false :=
exists.elim h
( assume barber,
begin
intro h,
have hbarber : shaves barber barber ↔ ¬shaves barber barber,
from h barber,
have nsbb : ¬shaves barber barber, from
assume sbb : shaves barber barber,
show false, from hbarber.mp sbb sbb,
show false, from nsbb (hbarber.mpr nsbb)
end
)
#print NoSuchBarber


#### Kevin Buzzard (Aug 14 2020 at 12:29):

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber : ¬ (∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y ) :=
λ ⟨x, hx⟩, (not_iff_self _).1 (hx x).symm


#### Kevin Buzzard (Aug 14 2020 at 12:29):

That's the mathlib proof

#### Norbert Bátfai (Aug 14 2020 at 12:31):

Kevin Buzzard said:

import tactic

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber ( h : ∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y )
: false :=
exists.elim h
( assume barber,
begin
intro h2, -- I don't want two hypotheses called h
have hbarber := h2 barber, -- human-generated good idea
tauto!, -- computer can finish it off
end
)


Thanks, your tactical proof is amazing. I am a newbie, but for me, it shows very well the power of the interactive nature of Lean.

#### Kevin Buzzard (Aug 14 2020 at 12:31):

import tactic

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber : ¬ (∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y ) :=
begin
rintros ⟨barber, h2⟩,
have hbarber := h2 barber,
library_search,
end


Here's a proof discovered by a computer after the good idea is input.

#### Kevin Buzzard (Aug 14 2020 at 12:32):

I cannot get the computer to have the good idea itself :-(

#### Ruben Van de Velde (Aug 14 2020 at 12:33):

Going the manual way:

variables (Man : Type) (shaves : Man → Man → Prop)
theorem NoSuchBarber ( h : ∃ x : Man,  ∀ y : Man, shaves x y ↔ ¬ shaves y y )
: false :=
exists.elim h
( λ barber h,
have hbarber : shaves barber barber ↔ ¬shaves barber barber := h barber,
have nsbb : ¬shaves barber barber := λ sbb, hbarber.mp sbb sbb,
nsbb (hbarber.mpr nsbb))
#print NoSuchBarber


#### Chris Wong (Aug 14 2020 at 12:34):

@Kevin Buzzard a bit unfortunate that tauto (without the !) doesn't work, since the manual proof seems to be constructive :pensive:

#### Kenny Lau (Aug 14 2020 at 12:48):

@Norbert Bátfai here's your code minimally modified to follow the spacing conventions (indent with 2 spaces, no space after opening bracket and before closing bracket, don't start a line with a punctuation except brackets), and also to remove the use of tactic mode (your proof does not actually need tactic mode):

theorem NoSuchBarber (Man : Type) (shaves : Man → Man → Prop)
(h : ∃ x : Man, ∀ y : Man, shaves x y ↔ ¬shaves y y) :
false :=
exists.elim h $assume barber : Man, assume h : ∀ y : Man, shaves barber y ↔ ¬shaves y y, have hbarbermpr : ¬shaves barber barber → shaves barber barber, from iff.mpr (h barber), have hbarbermp : shaves barber barber → ¬shaves barber barber, from iff.mp (h barber), have nsbb : ¬shaves barber barber, from assume sbb : shaves barber barber, show false, from hbarbermp sbb sbb, show false, from nsbb (hbarbermpr nsbb)  #### Norbert Bátfai (Aug 14 2020 at 12:54): Chris Wong said: I guess it comes down to context. If the purpose of the code snippet is to demonstrate Lean to a lay audience, then having all the intermediate steps spelled out can be helpful. But someone writing for mathlib – whose audience is experienced Lean programmers – would use a much terser style. I am interested in the case of "lay audience". Because I am looking for the opportunity to desing a First Ordel Logic-based game. My idea is for players to formalize their relationships and everyday activities. Until recently I have been thinking about a combination of FOL and Prolog, but now I really liked the Lean. #### Chris Wong (Aug 14 2020 at 13:03): Sounds great! I assume you've heard of the Natural Number Game? Perhaps you can reuse the infrastructure for that. #### Norbert Bátfai (Aug 14 2020 at 13:52): Thanks, and yes, I have played with it. From the point of view of education, it is a great gamification app for mathematical logic and especially the Lean. But I think, from the point of view of gaming, it seems like learning math rather than gaming. Unfortunately, I don’t have such a good idea of how to make a new League of legends or CS:GO on a logical basis either :) I am thinking of a simple secret diary written in a visual or math language where additional knowledge can be generated from the knowledge entered. Now that I have met the Lean, I am thinking about organizing a game around this ITP. I don’t have a specific idea for a rapid prototype for experimenting game-experience, but I am looking at pages that You mentioned, for example https://github.com/mpedramfar/Lean-game-maker or https://github.com/ImperialCollegeLondon/natural_number_game #### Norbert Bátfai (Aug 14 2020 at 14:07): Thanks for your pieces of advice. They are merged with Eric Wieser's modification: theorem NoSuchBarber (Man : Type) (shaves : Man → Man → Prop) (h : ∃ x : Man, ∀ y : Man, shaves x y ↔ ¬shaves y y) : false := exists.elim h$
assume barber : Man,
assume h : ∀ y : Man, shaves barber y ↔ ¬shaves y y,
have hbarber : shaves barber barber ↔ ¬shaves barber barber,
from h barber,
have nsbb : ¬shaves barber barber, from
assume sbb : shaves barber barber,
show false, from hbarber.mp sbb sbb,
show false, from nsbb (hbarber.mpr nsbb)


I was using tactical mode mainly because in this mode I was able to trace the operation of Lean well.

#### Eric Wieser (Aug 14 2020 at 14:18):

I remember hearing that the proof state was now traceable in term mode, but I didn't find that to be the case on the online lean compiler. Did I imagine it? Is that feature restricted to vs-code?

#### Kenny Lau (Aug 14 2020 at 14:19):

you just need to know the undocumented underscore trick

#### Kenny Lau (Aug 14 2020 at 14:20):

the only reason tactic mode is more popular is because NNG popularized tactic-mode Lean

#### Kenny Lau (Aug 14 2020 at 14:20):

but term mode is as easy to use as tactic mode

at least for me

#### Johan Commelin (Aug 14 2020 at 14:21):

Kenny Lau said:

the only reason tactic mode is more popular is because NNG popularized tactic-mode Lean

Mwahh, tactic mode was popular before NNG existed

#### Johan Commelin (Aug 14 2020 at 14:22):

I think Eric is talking about inspecting the proof state of a term-mode proof after it has been written. This feature was added 2 months ago (or somewhere around then).

#### Johan Commelin (Aug 14 2020 at 14:22):

I have no idea if it is supposed to work in the web editor.

#### Johan Commelin (Aug 14 2020 at 14:22):

I think it greatly improved the readability of term-mode proofs.

#### Bryan Gin-ge Chen (Aug 14 2020 at 14:23):

The community web editor should be on the same version of Lean as mathlib master. Can you show an example?

#### Eric Wieser (Aug 14 2020 at 14:31):

My example is the proofs above. I can't seem to stick my cursor anywhere to get something useful

#### Eric Wieser (Aug 14 2020 at 14:31):

Relatedly, I'm finding that import data.subtype works locally but fails on the web editor - is the web editor mathlib-less?

#### Bryan Gin-ge Chen (Aug 14 2020 at 14:33):

Are you using the community web editor? Here's the link to the barber paradox.

I do see the types as I move my cursor around: Screen-Shot-2020-08-14-at-10.32.03-AM.png

#### Eric Wieser (Aug 14 2020 at 14:40):

Nope, I was using the other one...

#### Utensil Song (Aug 14 2020 at 14:52):

I strongly believe that the proof should be as readable as the same proof in natural language:

import tactic

variables (Man : Type) (shaves : Man → Man → Prop)

theorem NoSuchBarber ( h : ∃ barber : Man,  ∀ m : Man, shaves barber m ↔ ¬ shaves m m )
: false :=
begin
-- from the existence of such a barber,
-- we obtain a barber and the associated hypothesis
obtain ⟨barber, barber_shaves_only_who_doesnt_self_shave⟩ := h,
-- apply the associated hypothesis to the barber (as a customer)
have self_shaving_dilemma := barber_shaves_only_who_doesnt_self_shave barber,
-- apply (a ↔ ¬a) → false to shaves barber barber as a
have dilemma_implies_false := (iff_not_self (shaves barber barber)).mp,
-- apply the theorem "dilemma implies false" to the fact that
-- we have proven the self-shaving dilemma
exact dilemma_implies_false self_shaving_dilemma
end


#### Alex J. Best (Aug 14 2020 at 16:01):

There have been several interesting advances recently on making simple games with graphical interfaces in lean (using the Widgets setup), like rubiks cube https://github.com/kendfrey/rubiks-cube-group and sudoku https://github.com/TwoFX/sudoku

#### Gabriel Ebner (Aug 14 2020 at 16:50):

Do you have a screenshot/example file for the Rubik's cube?

#### Kevin Buzzard (Aug 14 2020 at 16:52):

Some screenshots here https://twitter.com/XenaProject/status/1289450598530654208?s=20 . I don't think the code is public yet.

#### Kevin Buzzard (Aug 14 2020 at 16:57):

@Kendall Frey how does it work?

#### Kevin Buzzard (Aug 14 2020 at 17:03):

he tells me that you can put stuff like #html (R2 L2 U2 D2 F2 B2).to_html at the bottom of src/rubiks_cube.lean to get stuff like cube.png

#### Kendall Frey (Aug 14 2020 at 17:06):

Yes, it's not an interactive game though. It renders a cube state as a human-readable picture, as a fancier form of has_repr

#### Kevin Buzzard (Aug 14 2020 at 17:13):

one person's repo which renders a cube state as a human-readable picture is another person's game

#### Eric Wieser (Aug 14 2020 at 19:30):

Can to_html emit JavaScript with a webgl 3d canvas?

#### Kendall Frey (Aug 15 2020 at 00:59):

HTML widgets don't support JS as far as I know.

#### Chris Wong (Aug 15 2020 at 02:09):

Surely that's an artificial restriction, as the VS Code extension itself is written in JavaScript.

#### Mario Carneiro (Aug 15 2020 at 02:16):

there are security concerns, of course...

#### Chris Wong (Aug 15 2020 at 02:21):

Of course! A less (?) dangerous solution would be to define custom elements on the VS Code side, and have the Lean use those.

#### Mario Carneiro (Aug 15 2020 at 02:21):

however from what I can tell vscode-lean has disabled all the security restrictions, so it's probably just a lack of implementation in the widget impl

#### Chris Wong (Aug 15 2020 at 03:55):

I think also since tactics can run arbitrary code already, the only situation where that makes a difference is when using a remote editor, as in that case the compiler and editor are running in separate contexts

#### Norbert Bátfai (Sep 22 2020 at 06:46):

I tried to describe my thoughts: https://arxiv.org/abs/2009.09068

#### Edward Ayers (Nov 12 2020 at 18:04):

wrt the 3D stuff; right now with widgets you can only output an html DOM object for the infoview to render, so you can do svg and CSS transformations and even CSS animations, but no arbitrary javascript yet.

Last updated: May 13 2021 at 20:13 UTC