1
00:00:00,000 --> 00:00:3,000
Welcome, everybody.

2
00:00:3,000 --> 00:00:5,000
Welcome, colleagues.

3
00:00:5,000 --> 00:00:8,000
This is a joint talk with my two colleagues,

4
00:00:8,000 --> 00:00:13,500
Saksham Attri from India and Aaron Windischbauer from
Austria.

5
00:00:13,500 --> 00:00:16,000
It's about GNU Aris.

6
00:00:16,000 --> 00:00:20,000
It is a web application right now for students.

7
00:00:20,000 --> 00:00:24,500
It used to be a native application written in C,

8
00:00:24,500 --> 00:00:31,500
but now it's a C/C++ application for logic teaching

9
00:00:31,500 --> 00:00:34,000
mostly at university level.

10
00:00:34,000 --> 00:00:41,000
Thanks so much, Pilar, that you help us delivering this
talk.

11
00:00:42,000 --> 00:00:43,000
The logic education

12
00:00:43,000 --> 00:00:47,000
software tool GNU Aris is quite well known

13
00:00:47,000 --> 00:00:50,000
in the free software community,

14
00:00:50,000 --> 00:00:56,000
has been developed since 2011 by a GNU activist, Ian Dunn.

15
00:00:56,000 --> 00:01:01,500
It is no longer maintained by him, but the community,

16
00:01:01,500 --> 00:01:04,500
started to work on the project and

17
00:01:04,500 --> 00:01:11,500
now we have a new version and we have some new experiences

18
00:01:11,500 --> 00:01:17,500
how it works in some school situations, some classroom situations.

19
00:01:17,500 --> 00:01:21,000
This development was mostly based on the

20
00:01:21,000 --> 00:01:27,500
Google Summer of Code 2023 project and the biggest

21
00:01:27,500 --> 00:01:31,000
aim was to bring GNU Aris to the web application 

22
00:01:31,000 --> 00:01:39,500
and finally to try if the new features really applicable

23
00:01:39,500 --> 00:01:45,500
in classroom situations for university students who attend a logic course.

24
00:01:45,500 --> 00:01:48,500
You can ask the question: why another software tool?

25
00:01:48,500 --> 00:01:52,000
There are a lot of software tools,

26
00:01:52,000 --> 00:01:56,500
for example, the Coq system, Isabelle, Lean, and a lot

27
00:01:56,500 --> 00:01:57,500
of others.

28
00:01:57,500 --> 00:02:02,500
There are a lot of systems there to study mathematics or
other

29
00:02:03,000 --> 00:02:05,000
science research fields.

30
00:02:05,000 --> 00:02:06,000
As I said, GNU Aris,

31
00:02:06,000 --> 00:02:08,000
is not really new. Also,

32
00:02:09,000 --> 00:02:10,000
we think that

33
00:02:10,000 --> 00:02:12,000
the other big players

34
00:02:12,000 --> 00:02:14,000
like Coq or

35
00:02:14,000 --> 00:02:16,000
Lean or Isabelle, so they are

36
00:02:16,000 --> 00:02:18,000
very good, very big, but maybe

37
00:02:18,000 --> 00:02:19,000
too complex, too

38
00:02:19,000 --> 00:02:22,000
big, too difficult for

39
00:02:22,000 --> 00:02:24,000
prospective mathematics teachers.

40
00:02:24,000 --> 00:02:25,000
So, at least

41
00:02:25,000 --> 00:02:28,000
these young people who

42
00:02:28,000 --> 00:02:30,000
want to teach mathematics for

43
00:02:30,000 --> 00:02:32,000
the next generation, they are

44
00:02:32,000 --> 00:02:34,000
usually not familiar with programming.

45
00:02:35,000 --> 00:02:36,000
So, if they come

46
00:02:36,000 --> 00:02:37,000
to learn

47
00:02:37,000 --> 00:02:40,000
a system like Coq, it's really,

48
00:02:40,000 --> 00:02:41,000
really exhausting.

49
00:02:42,000 --> 00:02:44,000
It's really a big challenge

50
00:02:44,000 --> 00:02:46,000
and that's why it

51
00:02:46,000 --> 00:02:47,000
seems to be a good idea

52
00:02:47,000 --> 00:02:50,000
to give them something

53
00:02:50,000 --> 00:02:51,000
simpler.

54
00:02:51,000 --> 00:02:54,000
The other idea, the

55
00:02:54,000 --> 00:02:56,000
other concept is that

56
00:02:56,000 --> 00:02:58,000
usually you don't have to give a
whole

57
00:02:58,000 --> 00:03:00,000
system for these... students,

58
00:03:01,000 --> 00:03:02,000
prospective teachers.

59
00:03:03,000 --> 00:03:04,500
Because

60
00:03:04,500 --> 00:03:07,500
They usually need only a "taste" of the thing.

61
00:03:07,500 --> 00:03:10,500
So they don't need the whole system.

62
00:03:10,500 --> 00:03:13,500
They don't want to prove everything in
mathematics.

63
00:03:13,500 --> 00:03:17,500
They want to study just a small part of,

64
00:03:17,500 --> 00:03:22,500
for example, number theory or a very small part of calculus.

65
00:03:22,500 --> 00:03:28,500
It should be balanced between these two.

66
00:03:28,500 --> 00:03:32,500
We need to have a quite good working, nicely working system.

67
00:03:32,500 --> 00:03:36,500
On the other hand, it should be somewhat limited.

68
00:03:37,500 --> 00:03:42,500
So the syntax should be very close to the everyday
mathematics, to the school mathematics.

69
00:03:42,500 --> 00:03:47,000
But of course, it's quite good if

70
00:03:47,000 --> 00:03:53,500
there are still possibilities to reach a high level of mathematics in some sense.

71
00:03:54,500 --> 00:03:56,500
Why GNU Aris? It's because it's open source.

72
00:03:57,500 --> 00:04:02,500
It's complicated enough to tell some more complex stories

73
00:04:02,500 --> 00:04:03,500
for our students.

74
00:04:03,500 --> 00:04:05,500
But on the other hand,

75
00:04:06,000 --> 00:04:10,000
not really ready for end users... 

76
00:04:10,000 --> 00:04:14,000
at least at that time we started this project we learned that it's

77
00:04:15,000 --> 00:04:18,500
not easy to install it... among others... 

78
00:04:18,500 --> 00:04:23,000
so it has to be compiled and most students... most

79
00:04:23,000 --> 00:04:28,000
mathematics teacher students... they don't have an idea
on how to do it!

80
00:04:28,000 --> 00:04:33,000
Of course it's possible to compile the software for many platforms:

81
00:04:33,000 --> 00:04:35,000
for Windows, for Linux, for

82
00:04:35,000 --> 00:04:42,000
Mac, and we did it but it's sometimes also difficult to do something in the classroom

83
00:04:43,000 --> 00:04:45,500
even for university students because

84
00:04:45,500 --> 00:04:50,000
the computer room is limited for a web browser, so

85
00:04:50,000 --> 00:04:57,000
you don't...  have any access to install new systems,
new programs, so it's quite difficult...

86
00:04:57,000 --> 00:05:02,500
so a web version... seems to be a good option.

87
00:05:02,500 --> 00:05:05,500
Then the other thing is

88
00:05:05,000 --> 00:05:07,000
that for

89
00:05:07,500 --> 00:05:14,500
mathematics teachers: the native tongue.
The mother tongue is of course preferred.

90
00:05:14,500 --> 00:05:22,000
Then the import-export part of GNU Aris was also not really
standard.

91
00:05:22,500 --> 00:05:31,500
It's in XML format... we were thinking about that. And unfortunately the user can

92
00:05:31,500 --> 00:05:38,500
experience some crashes in some situations.
Well, in this slide you can

93
00:05:38,500 --> 00:05:42,500
see how the old version looked like.

00:05:42,500 --> 00:05:46,500
It's a modern system in some sense, so it has

94
00:05:46,500 --> 00:05:49,500
a so-called GTK interface.

95
00:05:49,500 --> 00:05:53,500
Well, you can see: on the top there is a menu.

96
00:05:53,500 --> 00:06:00,500
Then statements that are commented with
arbitrary

97
00:06:00,500 --> 00:06:01,500
long texts.

98
00:06:01,500 --> 00:06:09,500
Then you can tell if this line is a... is a premise
or

99
00:06:09,500 --> 00:06:13,000
maybe a conclusion of the older... premises
and

100
00:06:14,000 --> 00:06:18,000
while "dm" is the De Morgan rule

101
00:06:18,000 --> 00:06:20,000
so any

102
00:06:22,000 --> 00:06:26,000
line here is kind of application of the De Morgan
rule

103
00:06:27,000 --> 00:06:30,000
Yes, so back to Google Summer of Code.

104
00:06:30,000 --> 00:06:34,000
We are very grateful to Google that they supported this
project.

105
00:06:34,000 --> 00:06:39,000
Mostly the work was done by Saksham in
India.

106
00:06:39,000 --> 00:06:47,000
It was three months of very active work with some support by
two more students

107
00:06:48,000 --> 00:06:52,000
Andreas Ebetshuber and Alexander Thaller and I
was

108
00:06:53,000 --> 00:06:57,000
responsible for mentoring the whole project.
We had a work plan.

109
00:06:58,000 --> 00:07:01,000
It's necessary when you start some of Google Code
project.

110
00:07:02,000 --> 00:07:04,000
It consisted of five

111
00:07:04,000 --> 00:07:09,000
big steps to create a so-called Qt interface.
The Qt

112
00:07:09,000 --> 00:07:11,000
system

113
00:07:11,000 --> 00:07:16,500
allows programming in a framework,
C++ framework.

114
00:07:16,500 --> 00:07:22,500
And because of that, it was possible to compile the whole
system

115
00:07:22,500 --> 00:07:27,500
into HTML and WebAssembly, which means much more
flexibility.

116
00:07:28,500 --> 00:07:31,500
Then the interface had to be polished a
bit.

117
00:07:32,500 --> 00:07:37,500
We published a new version, and then we started to get user
feedback

118
00:07:37,500 --> 00:07:39,500
and to fix issues.

119
00:07:39,500 --> 00:07:42,500
Maybe you want to know what is this big A
here.

120
00:07:42,500 --> 00:07:49,500
This is the logo of GNU Aris, and it was designed by Ian
Dunn,

121
00:07:49,500 --> 00:07:51,500
original developer of the program.

122
00:07:52,500 --> 00:07:54,500
So he is Saksham.

123
00:07:54,500 --> 00:08:00,500
He is a young student in India,
and he worked hard on the implementation.

124
00:08:01,500 --> 00:08:06,500
He takes the lead now and gives some details on the
implementation.

125
00:08:07,500 --> 00:08:09,500
I will now explain the architectural.

126
00:08:09,500 --> 00:08:11,500
design for the Qt
application.

127
00:08:12,000 --> 00:08:16,000
Here, we have tried to emulate the famous
model-view-controller framework.

128
00:08:16,000 --> 00:08:22,000
So, the user's interaction is limited to the view,
which, in this case, is provided

129
00:08:22,000 --> 00:08:24,000
by the QML UI.

130
00:08:24,000 --> 00:08:29,000
If the user request exceeds capabilities built into the UI,
then the request is forwarded

131
00:08:29,000 --> 00:08:34,000
to a C++ controller layer, along with the relevant proof
data.

132
00:08:34,000 --> 00:08:36,000
This middle layer now processes the data into 

133
00:08:36,000 --> 00:08:39,000
appropriate C data types, and forwards it

134
00:08:39,000 --> 00:08:41,000
to the C logic engine.

135
00:08:41,000 --> 00:08:43,000
We are reusing the old logic engine

136
00:08:43,000 --> 00:08:47,000
by decoupling the GTK UI with program logic.

137
00:08:47,000 --> 00:08:51,000
Thus, the generated results are communicated back to the
controller,

138
00:08:51,000 --> 00:08:52,500
which then updates the view 

139
00:08:52,500 --> 00:08:55,500
so that the results are displayed to the user.

140
00:08:57,000 --> 00:09:05,000
While the new interface is a bit different from the GTK interface, it was quite important

141
00:09:05,000 --> 00:09:15,000
to create a new kind of user interface that is transparent
in the sense of working in

142
00:09:15,000 --> 00:09:24,000
a native environment, so natively in Windows,
on Mac, on Linux, but also to be able to

143
00:09:24,000 --> 00:09:26,000
translate it into the web.

144
00:09:26,000 --> 00:09:33,000
So what you can see here, this is the native version of the
new Qt version,

145
00:09:33,000 --> 00:09:39,000
again with the same premises and the same conclusions.

146
00:09:39,000 --> 00:09:42,000
Conclusion is the notion here in GNU Aris.

147
00:09:42,000 --> 00:09:50,500
And the menu system is a bit different,
so here you can open the menu,

148
00:09:50,500 --> 00:09:54,000
and also there is a virtual keyboard to

149
00:09:54,000 --> 00:09:58,000
enter logical operations and some other
symbols,

150
00:09:58,500 --> 00:10:04,500
finally this button here is responsible for checking if
you

151
00:10:06,500 --> 00:10:12,500
typed the input correctly or not... so if it is not correct
then you will get a red

152
00:10:13,500 --> 00:10:22,500
color here... the other interface... the web interface is 

153
00:10:18,000 --> 00:10:22,500
quite similar... of course there are some very

154
00:10:22,500 --> 00:10:29,500
minor differences. This example here is a bit different and
you can see that there is

155
00:10:30,500 --> 00:10:38,500
an option to write the mathematical symbols... somewhat
differently 

156
00:10:38,500 --> 00:10:40,500
okay so let's start this

157
00:10:40,500 --> 00:10:48,500
program... if you... start GNU Aris... well yeah maybe it's... 

158
00:10:48,500 --> 00:10:51,500
it's not bad to start it again

159
00:10:51,500 --> 00:10:51,500
so in

160
00:10:52,500 --> 00:11:00,000
in background the WebAssembly code is compiled and here this is one

161
00:11:00,000 --> 00:11:07,500
input line... well I add a statement A and I add a new premise:

162
00:11:07,500 --> 00:11:12,000
statement B and then I add the conclusion:

163
00:11:12,000 --> 00:11:18,500
it's A and B. A and B is a conclusion.

164
00:11:18,500 --> 00:11:26,000
Now if I try to check if it is okay, then we get an error message...

165
00:11:26,000 --> 00:11:32,000
that... well, there is a default rule set and a default rule and

166
00:11:32,000 --> 00:11:36,000
here we didn't really use the

167
00:11:36,000 --> 00:11:43,000
inference... the inference group and modus ponens but we used
something different... 

168
00:11:43,000 --> 00:11:44,000
here we used the

169
00:11:44,000 --> 00:11:53,000
conjunction and now if you click on it, it is still an error
because we need to give the references

170
00:11:54,000 --> 00:11:55,000
to the premises.

171
00:11:56,000 --> 00:11:59,000
So what is the first premise... first

172
00:12:01,500 --> 00:12:09,500
reference: this one and this one, so the cursor needs to be
here and we need to click on the

173
00:12:10,500 --> 00:12:19,500
reference so now we can see that this conjunction is related
to one and two... or is this based on

174
00:12:19,500 --> 00:12:33,500
these two premises and if we click on evaluate and we get
this answer. Well, if we remove something,

175
00:12:33,500 --> 00:12:39,500
you can try it again... you can see that those lines that are
syntactically correct,

176
00:12:39,500 --> 00:12:46,500
they are still green. Only those lines that have some
problems in the background: they are red.

177
00:12:49,500 --> 00:12:57,500
Back to the presentation. We managed to hold a series of
lectures on logic. My former student

178
00:12:57,500 --> 00:13:00,000
and my colleague now, 

179
00:13:00,000 --> 00:13:10,500
Aaron, was one of these 30 students between October 2023 and January 2024.

180
00:13:10,500 --> 00:13:20,500
So he also tried the program, he gave feedback,
and some examples were done by him.

181
00:13:20,500 --> 00:13:28,500
Well, this logic course discussed two main topics,
propositional logic and first-order logic.

182
00:13:28,500 --> 00:13:34,500
Of course, 15 weeks are not too much for such big
topics.

183
00:13:34,500 --> 00:13:39,500
With GNU Aris... GNU Aris was not the only software system
we used...

184
00:13:40,500 --> 00:13:46,500
to visualize, to explain some concepts of logic,
we used other systems,

185
00:13:46,500 --> 00:13:50,500
for example, GeoGebra Discovery,
or a SAT solver, MiniSAT.

186
00:13:51,000 --> 00:13:57,000
Mathematica, Wolfram Alpha for propositional logic too.

187
00:13:57,000 --> 00:14:03,000
Here we would like to illustrate GNU Aris with two
examples.

188
00:14:03,000 --> 00:14:09,000
One example is from a quite well-known book,
from Raymond Smullyan,

189
00:14:09,000 --> 00:14:13,000
the famous logician, The Lady or the
Tiger.

190
00:14:13,000 --> 00:14:20,000
And the second example is a well-
known basic concept from category
theory.

191
00:14:20,000 --> 00:14:23,000
So let's have a look.

192
00:14:23,000 --> 00:14:33,000
The first example is shown in German,
because this is how it is authentic. :-)

193
00:14:33,000 --> 00:14:39,000
It's about a king who gives a puzzle for the
prisoners.

194
00:14:39,000 --> 00:14:43,000
So maybe you want to see this question in
English.

195
00:14:43,000 --> 00:14:49,000
The basic idea will be explained in the next
slide.

196
00:14:49,000 --> 00:14:50,000
So the king...

197
00:14:50,000 --> 00:14:53,000
tries to find good puzzles

198
00:14:52,500 --> 00:14:53,500
for the prisoners.

199
00:14:53,500 --> 00:14:57,500
Well, let me read this.

200
00:14:57,500 --> 00:15:01,500
Yesterday was a fiasco, said the king to his
minister.

201
00:15:01,500 --> 00:15:04,500
The three prisoners solved their
puzzles.

202
00:15:04,500 --> 00:15:10,500
Well, we have five trials coming up today,
and I think I'll make them a little
tougher.

203
00:15:10,500 --> 00:15:13,500
"Excellent idea", said the minister.

204
00:15:13,500 --> 00:15:19,500
Well, in each of the trials of this day,
the king explained that in the left-hand room

205
00:15:19,500 --> 00:15:24,500
(room 1), if a lady is in it, then the sign on the door is
true.

206
00:15:24,500 --> 00:15:27,500
But if a tiger is in it, the sign is
false.

207
00:15:27,500 --> 00:15:32,500
In the right-hand room (room 2),
the situation is the
opposite.

208
00:15:32,500 --> 00:15:36,500
A lady in the room means the sign on the door is false,
and the tiger in the room means

209
00:15:36,500 --> 00:15:38,500
the sign is true.

210
00:15:38,500 --> 00:15:45,500
Again, it is possible that both rooms contain ladies or both
rooms contain tigers, or that

211
00:15:45,500 --> 00:15:47,500
one room contains a lady and the other a
tiger.

212
00:15:49,500 --> 00:15:56,000
This is the English explanation, the English story of the puzzle.

213
00:15:56,000 --> 00:16:00,500
So the puzzle is exactly the fifth trial.

214
00:16:00,500 --> 00:16:06,500
Same rules apply, and here are the signs. At least one room contains a lady,

215
00:16:06,500 --> 00:16:15,500
room one, and room two, the other room contains a lady.
So this is the fifth puzzle. Here

216
00:16:15,500 --> 00:16:22,500
you can see the Hungarian version of this book,
a very famous, very well-known book.

217
00:16:22,500 --> 00:16:30,500
And here Aaron shows the German translation,
also quite popular.

218
00:16:30,500 --> 00:16:33,500
Now Aaron will tell you

219
00:16:33,500 --> 00:16:40,500
some words how he solved this problem when he was a member
of this course.

220
00:16:43,500 --> 00:16:48,500
As already stated, this is my solution to Smullyan's fifth
trial in the web version of GNU Aris.

230
00:16:48,500 --> 00:16:52,500
I started with premises which represent the rules of the
trial,

231
00:16:52,500 --> 00:16:54,500
where L and T followed by a number

232
00:16:54,500 --> 00:16:59,000
to indicate that there is a lady or a tiger in that specific room.

233
00:16:59,000 --> 00:17:01,500
S1 and S2 refer to the signs of

234
00:17:01,500 --> 00:17:07,500
each room. Then I initiated a sub-
proof with the assumption of a lady being in room 2.

235
00:17:07,500 --> 00:17:13,500
With the rules of the trial, I deduced that the assumption leads to a negation of sign 1,

236
00:17:13,500 --> 00:17:16,500
which means there is no lady in any of the rooms.

237
00:17:16,500 --> 00:17:19,500
This leads to a contradiction with the assumption that there

238
00:17:19,500 --> 00:17:21,500
is a lady in room 2.

239
00:17:21,500 --> 00:17:27,500
This figure shows how I used that contradiction, which indicates that a tiger

240
00:17:27,500 --> 00:17:30,000
must be in room 2. With that information,

241
00:17:30,000 --> 00:17:32,500
I deduced that the sign of room 2 is true,

242
00:17:32,500 --> 00:17:35,500
and therefore a lady has to be in room 1.

243
00:17:35,500 --> 00:17:37,500
I finished the proof by showing that a lady in

244
00:17:37,500 --> 00:17:42,000
room 1 does not lead to a contradiction.

245
00:17:42,000 --> 00:17:44,500
A lady in room 1 means that the statement of sign

246
00:17:45,000 --> 00:17:46,000
one of at least one room

247
00:17:46,000 --> 00:17:48,000
containing a lady is true

248
00:17:48,000 --> 00:17:50,000
which does not contradict that

249
00:17:50,000 --> 00:17:52,000
a lady is in room one. The final

250
00:17:52,000 --> 00:17:54,000
line is the solution of the puzzle.

251
00:17:55,000 --> 00:17:56,000
The prisoner should pick room one

252
00:17:56,000 --> 00:17:58,000
since that room contains a lady.

253
00:17:59,000 --> 00:18:00,000
The second

254
00:18:00,000 --> 00:18:02,000
example about

255
00:18:02,000 --> 00:18:05,000
a so-called binary operation

256
00:18:05,000 --> 00:18:06,000
is denoted

257
00:18:06,000 --> 00:18:08,000
by O. It has

258
00:18:08,000 --> 00:18:09,000
two parameters

259
00:18:09,000 --> 00:18:13,000
and we assume that this operation

260
00:18:13,000 --> 00:18:14,000
is commutative.

261
00:18:15,000 --> 00:18:16,000
Because it

262
00:18:16,000 --> 00:18:18,000
is assumed for each a

263
00:18:18,000 --> 00:18:20,000
and for each b. And we

264
00:18:20,000 --> 00:18:22,000
assume that there is

265
00:18:22,000 --> 00:18:24,000
a so-called

266
00:18:24,000 --> 00:18:27,000
right

267
00:18:27,000 --> 00:18:28,000
identity element

268
00:18:28,000 --> 00:18:30,000
which means that for each a

269
00:18:30,000 --> 00:18:33,000
this binary operation

270
00:18:33,000 --> 00:18:34,000
delivers a.

271
00:18:35,000 --> 00:18:37,000
So this is a kind

272
00:18:37,000 --> 00:18:38,000
of neutral thing or

273
00:18:38,000 --> 00:18:41,000
as other formulated

274
00:18:41,000 --> 00:18:42,000
it's a right

275
00:18:42,000 --> 00:18:44,000
identity. Then by

276
00:18:44,000 --> 00:18:46,000
using some rule

277
00:18:46,500 --> 00:18:58,500
we can learn that for each a is "a operation e_"
equals a so this

278
00:18:58,500 --> 00:19:05,500
is because the second statement this is a so-
called existential instantiation

279
00:19:05,500 --> 00:19:15,000
in GNU Aris. Then you can use the commutative property

280
00:19:15,000 --> 00:19:21,000
and so on... so for each step there was a rule in GNU Aris.

281
00:19:21,000 --> 00:19:32,500
Finally you can learn that there is an "f", element of the main set that

282
00:19:36,000 --> 00:19:38,000
this identity also holds.

283
00:19:38,000 --> 00:19:39,000
So a right identity

284
00:19:39,000 --> 00:19:41,000
element is also a left

285
00:19:41,000 --> 00:19:43,000
identity element.

286
00:19:44,000 --> 00:19:45,000
And vice versa, it's not

287
00:19:45,000 --> 00:19:46,000
shown here.

288
00:19:48,000 --> 00:19:50,000
What kind of feedback we get

289
00:19:50,000 --> 00:19:51,000
from the other students,

290
00:19:52,000 --> 00:19:54,000
from the other 29...?

291
00:19:54,000 --> 00:19:55,000
And also Aaron

292
00:19:55,000 --> 00:19:57,000
was giving some

293
00:19:57,000 --> 00:19:59,000
feedback. Well, the

294
00:19:59,000 --> 00:20:01,000
error messages are not very

295
00:20:01,000 --> 00:20:04,000
easy to understand

296
00:20:04,000 --> 00:20:05,000
for simple

297
00:20:05,000 --> 00:20:07,000
users. It's for programmers

298
00:20:07,000 --> 00:20:09,000
more or less and not for

299
00:20:09,000 --> 00:20:11,000
simple users

300
00:20:11,000 --> 00:20:13,000
like prospective mathematics teachers.

301
00:20:14,000 --> 00:20:16,000
Then it

302
00:20:16,000 --> 00:20:17,000
should be not bad if

303
00:20:17,000 --> 00:20:19,000
some more feedback would

304
00:20:19,000 --> 00:20:21,000
be given for the user if there is

305
00:20:21,000 --> 00:20:23,000
an error. Some

306
00:20:23,000 --> 00:20:25,000
devices are not really supported if

307
00:20:25,000 --> 00:20:27,000
they have a small display.

308
00:20:27,000 --> 00:20:29,000
This is not very good

309
00:20:29,000 --> 00:20:31,000
at the moment yet.

310
00:20:32,000 --> 00:20:33,000
Changing the language

311
00:20:33,000 --> 00:20:35,000
to a different one

312
00:20:35,000 --> 00:20:37,000
than English... still

313
00:20:37,500 --> 00:20:38,500
on the wishlist.

314
00:20:38,500 --> 00:20:48,000
Copying, pasting, highlighting inputs, or to change the input type, of a statement... 

315
00:20:48,000 --> 00:20:52,500
is a technical question, but it should be nice to work.

316
00:20:52,500 --> 00:20:58,000
And also the exclusive disjunction and the contrapositive,

317
00:20:58,000 --> 00:21:03,500
they were missing for many proofs, and therefore our proofs were quite long.

318
00:21:03,500 --> 00:21:09,500
And some ideas could be implemented for the next year,

319
00:21:09,500 --> 00:21:15,000
so maybe we can have some more reports then.

320
00:21:16,500 --> 00:21:21,500
And that's all. Thank you so much for being here,

321
00:21:21,500 --> 00:21:29,500
and we want to share some references that could be
interesting if you want to learn more on
this.

322
00:21:30,500 --> 00:21:33,500
Well, we will hopefully continue this
project...

323
00:21:33,500 --> 00:21:38,500
in the next months, and we would like to do some
more...

324
00:21:39,000 --> 00:21:41,000
if possible. Thank you so

325
00:21:41,000 --> 00:21:43,000
much. We wish you a great

326
00:21:43,000 --> 00:21:45,000
conference evening

327
00:21:45,000 --> 00:21:47,000
and see you soon

328
00:21:47,000 --> 00:21:49,000
hopefully in person.