-
1
-
2
-
3
-
4
-
5
-
6
-
7
-
8
-
9
-
10
-
11
-
12
-
13
-
14
-
15
-
16
-
17
-
18
-
19
-
20
-
21
-
22
-
23
-
24
-
25
-
26
-
27
-
28
-
29
-
30
-
31
-
32
-
33
-
34
-
35
-
36
-
37
-
38
-
39
-
40
-
41
-
42
-
43
-
44
-
45
-
46
-
47
-
48
-
49
-
50
-
51
-
52
-
53
-
54
-
55
-
56
-
57
-
58
-
59
-
60
-
61
-
62
-
63
-
64
-
65
-
66
-
67
-
68
-
69
-
70
-
71
-
72
-
73
-
74
-
75
-
76
-
77
-
78
-
79
-
80
-
81
-
82
-
83
-
84
-
85
-
86
-
87
-
88
-
89
-
90
-
91
-
92
-
93
-
94
-
95
-
96
-
97
-
98
-
99
-
100
-
101
-
102
-
103
-
104
-
105
-
106
-
107
-
108
-
109
-
110
-
111
-
112
-
113
-
114
-
115
-
116
-
117
-
118
-
119
-
120
-
121
-
122
-
123
-
124
-
125
-
126
-
127
-
128
-
129
-
130
-
131
-
132
-
133
-
134
-
135
-
136
-
137
-
138
-
139
-
140
-
141
-
142
-
143
-
144
-
145
-
146
-
147
-
148
-
149
-
150
-
151
-
152
-
153
-
154
-
155
-
156
-
157
-
158
-
159
-
160
-
161
-
162
-
163
-
164
-
165
-
166
-
167
-
168
-
169
-
170
-
171
-
172
-
173
-
174
-
175
-
176
-
177
-
178
-
179
-
180
-
181
-
182
-
183
-
184
-
185
-
186
-
187
-
188
-
189
-
190
-
191
-
192
-
193
-
194
-
195
-
196
-
197
-
198
-
199
-
200
-
201
-
202
-
203
-
204
-
205
-
206
-
207
-
208
-
209
-
210
-
211
-
212
-
213
-
214
-
215
-
216
-
217
-
218
-
219
-
220
-
221
-
222
-
223
-
224
-
225
-
226
-
227
-
228
-
229
-
230
-
231
-
232
-
233
-
234
-
235
-
236
-
237
-
238
-
239
-
240
-
241
-
242
-
243
-
244
-
245
-
246
-
247
-
248
-
249
-
250
-
251
-
252
-
253
-
254
-
255
-
256
-
257
-
258
-
259
-
260
-
261
-
262
-
263
-
264
-
265
-
266
-
267
-
268
-
269
-
270
-
271
-
272
-
273
-
274
-
275
-
276
-
277
-
278
-
279
-
280
-
281
-
282
-
283
-
284
-
285
-
286
-
287
-
288
-
289
-
290
-
291
-
292
-
293
-
294
-
295
-
296
-
297
-
298
-
299
-
300
-
301
-
302
-
303
-
304
-
305
-
306
-
307
-
308
-
309
-
310
-
311
-
312
-
313
-
314
-
315
-
316
-
317
-
318
-
319
-
320
-
321
-
322
-
323
-
324
-
325
-
326
-
327
-
328
-
329
-
330
-
331
-
332
-
333
-
334
-
335
-
336
-
337
-
338
-
339
-
340
-
341
-
342
-
343
-
344
-
345
-
346
-
347
-
348
-
349
-
350
-
351
-
352
-
353
-
354
-
355
-
356
-
357
-
358
-
359
-
360
-
361
-
362
-
363
-
364
-
365
-
366
-
367
-
368
-
369
-
370
-
371
-
372
-
373
-
374
-
375
-
376
-
377
-
378
-
379
-
380
-
381
-
382
-
383
-
384
-
385
-
386
-
387
-
388
# Chars
define k = Character("Kublai", color="#A8836B")
define g = Character("The Go Gopher", color="#E994B2")
define s = Character("Saddam Hussein's LinkedIn (SHL)", color="#EB4653")
define f = Character("Fenwick", color="#D4CFDB")
# Rainbow shaking text
transform shake():
parallel:
matrixcolor TintMatrix("#FF0000") # Red
linear 0.1 matrixcolor TintMatrix("#FF7F00") # Orange
linear 0.1 matrixcolor TintMatrix("#FFFF00") # Yellow
linear 0.1 matrixcolor TintMatrix("#00FF00") # Green
linear 0.1 matrixcolor TintMatrix("#0000FF") # Blue (screw you indigo)
linear 0.1 matrixcolor TintMatrix("#8B00FF") # Violet
linear 0.1 matrixcolor TintMatrix("#FF0000") # Red again
repeat
parallel:
ease 0.05 xoffset -2 yoffset -1 rotate -1
ease 0.05 xoffset 1 yoffset 2 rotate 2
ease 0.05 xoffset -1 yoffset 2 rotate -2
ease 0.05 xoffset 2 yoffset -1 rotate 1
repeat
# Variant of say from screens.rpy
screen shake_say(who, what):
window:
id "window"
if who is not None:
window:
id "namebox"
style "namebox"
text who id "who"
text what id "what" at shake yalign 0.5 # idk why this specific number
# Skip the main menu and immediately start the game
label start:
scene bg codebase
show kublai
k "Huh?"
k "What are you doing here?"
menu:
"Uh...":
pass
"Good question!":
pass
"Wasting time, I guess?":
pass
label kublai_intro:
k "Well I'm not really sure what happened to the usual homepage, but I guess just, uh, close the tab maybe?"
k "You see, um, I'm not really being paid for this, so... not really sure what to say..."
k "Oh! I remember now! You should totally download Kublai: Star Rail right this instant! I definitely wasn't paid to say that, I swear!"
play music "push_ahead.ogg"
scene white with vpunch
show bg ksr at top with zoomin
k "Yes yes yes! Kublai: Star Rail! It's a critically acclaimed award-winning free-to-play turn-based mobile role-playing game, sequel to the one-and-only Genghis Impact!"
hide bg ksr
show bg gi at top
k "You've heard of Genghis Impact at least, right? I mean like, Genghis did have a pretty big impact."
hide bg gi
show bg ksr at top
k "Well, trust me, Kublai: Star Rail is just the best thing ever, like who wouldn't want to build galactic railroads for the glory of the equally critically acclaimed and award-winning Mongol Empire?"
show gopher at left with vpunch
show kublai at right
g "KUUUUBLAAAIIIII!!!" (screen="shake_say")
k "AAAAAAAAAHHHHHH!!!"
g "Yo Kublai! SHL's geniusly genius talk is gonna start in a few minutes! You gotta pull up! It's gonna be epic!"
k "Huh? What talk?"
g "Haven't heard the news? Our friend SHL is giving a really cool math talk at MIT and I can't even understand the talk's title but it sounds like pure awesomeness!"
k "Oh no, not SHL! She's always talking about useless niche math problems that only three people in the entire world care about!"
k "Why can't she do some actually useful math like optimization methods for the Genghis Impact leveling system!"
g "Oh come on Kublai! I'm using a sick day just to attend this talk! Usually I have to work all day keeping this website running!"
k "Wait... so the homepage is gone because you're slacking off?"
g "Yeah, this site uses the Caddy web server and the Hugo static site generator, both written in Go, so it's my job to keep them running smoothly 24/7!"
show gopher angry
k "Rewrite it in Rust!"
show gopher
k "Or even better, rewrite it in Dafny!"
g "Huh? What's Dafny?"
k "Dafny is a verification-aware programming language that makes it easy to mathematically prove properties about your code!"
k "Isn't that the coolest thing ever? Other than Kublai: Star Rail, of course."
k "I've even managed to prove that P equals NP using Dafny!"
g "COOL!! You gotta show me your proof sometime!" (screen="shake_say")
g "Wait OH SHOOT, I just realized we're gonna be late to SHL's talk! Let's get going!"
k "No way!"
g "Hey, I'll download Kublai: Star Rail if you come with me to this talk!"
k "Fine! But you have to leave a five-star review too!"
hide gopher with moveoutleft
k "Actually no, a six-star review!"
hide kublai with moveoutleft
play music "happy_timepass.ogg" fadeout 1.0
scene bg bathroom with dissolve
show shl at left with moveinleft
s "Hi everyone! I'm SHL the fox, and I'm the tenured head of mathematics at https://unnamed.website and listed as the coauthor on at least 69 research papers."
s "So, welcome to MIT! Sadly I couldn't book a lecture hall since actual classes are happening right now, so we'll have to use this venue instead."
s "But hey, it's by far the nicest shower in the basement of MIT's CS building!"
show kublai at right
k "So it's a mathroom, not a bathroom."
s "No it's a basement bathroom, not to be confused with a bathroom basement, which you would probably only have if you were an evil villain hiding your secret lair underneath your bathroom."
s "Anyways, today I'll be talking about the variational derivation of the wave equation using invariance under the Poincaré group."
hide kublai
show gopher at right with vpunch
g "YAAAAAAAAAAYYYYYY!!!" (screen="shake_say")
hide gopher
show fenwick at right
f "Sounds like a fascinating topic!"
hide fenwick
s "But before we start throwing around equations and tensors, I'd like to tell you a bit about {i}why{/i} I chose to give this talk,"
s "Because it's a lot of fun, because it's the synthesis of some elegant math concepts, because I've always wanted to add \"giving a talk at MIT\" to my resume,"
s "And well, sadly, 2025 is not exactly a year for, you know, old school continuum applied math."
s "It's the year, or at least the past few years have been the years of machine learning."
s "I'm still upset that they stole our tensors."
s "But the truth is that machine learning has really changed the world, how research is being done in applied math, how scams are conducted,"
s "And is leading lots of people to wonder whether it's important or not to study concepts of physics and continuum applied math, because discrete applied math seems to instasolve everything these days."
s "It's just all ML, ML, ML, ML-"
show kublai at right
k "What about OCaml?"
s "It's like ML for camels, I guess."
hide kublai
s "I mean, even I'm doing some machine learning nowadays, since people love it when you randomly add a completely unnecessary neural network to your project."
s "But I'm still convinced that it's quite possible that continuum applied math and physics might make a resurgence."
s "We're not exactly at a point where theoretical physics is very healthy. We don't have the same kind of, let's say, you know, interesting phenomena to model puzzles like we used to."
s "If you look back around 100 years ago, for instance, what was theoretical physics like?"
s "100 years ago, people were discovering quantum mechanics. It was super exciting."
show gopher at right with vpunch
g "YOU DON'T SOUND VERY EXCITED DO YOU?" (screen="shake_say")
hide gopher
s "Anyways, people didn't know how to understand the energy levels of the hydrogen atom, whether nature was deterministic or probabilistic,"
s "There was a flurry of activity, a bunch of discoveries, the main two of those being relativity and quantum mechanics,"
s "And that continued for a number of decades, maybe until the 60s with quantum field theory and particle physics and all of that. And then what happened since 1960?"
s "Well, many, many things happened, but not at the same level of like leaps in terms of progress."
s "And so if you look at what's happening in physics these days, it's not driven by the same kind of kind of on my questioning about basic things that used to be,"
s "We don't really have a sense of here's data we don't understand that we need to make sense of like. It's not exactly that."
s "It's like exotic materials and so forth, condensed matter, cosmology,"
s "But it's not like an immediate things that you want to understand. Why? Why is that so?"
s "What does that mean for the future of physics?"
s "I mean, I don't have to convince you that physics is in big crisis, right? The Nobel Prize in physics was awarded to machine learning!"
s "It's not saying just that machine learning is the hot new thing nowadays. It's also saying that there's a problem with business."
s "So I like to think of it as something's going to come up that will make these these, you know, math and physics of the continuum variety important again, and you have events that lead to that in particular."
s "I don't know. Think of four years ago. Let's go back to 2020 and COVID."
show kublai angry at right
k "Ugh, please no."
s "So COVID was March 2020. And where were you back then?"
k "Stop, I don't wanna relive the traumatic quarantine flashbacks!"
hide kublai
s "Maybe I can tell you what happened in my field around 2020. So from my perspective, from the research perspective, it got us to think about, what kind of research should we be doing?"
s "There was a moment where everybody wanted to be an epidemiologist."
s "I remember being brave enough to write Python scripts for modeling infectious diseases, you know, compartmental models and such."
s "So that was like an enormous peak of interest there and then. Like a few months later, the peak went way down, and the year after, nodody wanted to hear about it anymore."
s "And this idea they wanted to become an epidemiologist had passed."
s "So what I'm saying is that we need to be reactive to certain things that happen in society."
s "And do you remember when Gen AI happened and hit the scene, when ChatGPT came out?"
s "These are among those cataclysmic events now that we don't have relativity or quantum to drive what society is doing."
s "Because when future historians look back, they won't remember Shakespeare. They'll remember gpt-3.5-turbo-0301."
s "So it's very possible in my mind that we'll have more of these events in the in the decades to come."
s "We'll have more COVID, ChatGPT moments, I think in the future, and I think we'll come to a realization that physics is grossly incomplete and that might happen fairly soon."
s "And there's growing evidence that that's the case."
s "And it's not just a matter of looking at experiments from particle accelerators or telescopes, you know, in space and things like that,"
s "But there might be very accessible phenomena that makes us think that physics is actually grossly incomplete, and among those you have what are called {i}unidentified flying objects{/i}."
show fenwick angry at right with vpunch
play music "intense_momentloop.ogg"
f "WHAT??? UFOs? Are you insane? I thought you were a serious mathematician!"
s "I am! I'm very serious. And I can put on my glasses if you think I don't look smart enough."
f "SHL, I respect your intellect, but in fact I think you're also clever enough to convince yourself that you can't be wrong."
s "Look, this isn't the main topic of my talk. I just want you to be aware that there's an enormous amount of data out there on the internet about things we don't understand."
f "Can we move on already? You haven't said a single thing about the wave equation yet!"
hide fenwick
show gopher at right
g "HEY! I wanna hear her talk about UFOs! Maybe SHL is on to something!"
s "Sure, I can give some examples."
g "YIIIPPEEEE!!!" (screen="shake_say")
s "So you have billions and billions of observations of these airplanes in the sky which look and act exactly like commercial airplanes, but are actually UFOs piloted by extraterrestrials."
s "It's all to disguise the truth from us!"
s "And you have these crafts with handsfree telephony and advanced propulsion without wings or rotors that can defy physics and turn invisible or display a video of Bad Apple on themselves."
s "We're talking orbs. We're talking New Jersey orbs, right? And this comes from a YouTube comment."
s "And one of my friends recently changed her star sign, which I didn't even know was possible, but must be evidence of extraterrestrial interference!"
hide gopher
show kublai at right
k "Or maybe she just paid a large-enough bribe?"
s "Yes, yes, that's exactly what she did! She bribed the aliens!"
hide kublai
show fenwick at right
f "I think you need to go outside and eat grass."
s "I think you just need to look this up online, and you'll the data has been unequivocal about this."
s "Sure, debunking exists, but the debunking itself has been debunked!"
s "Nowadays these people say things are deepfakes. But I'm completely convinced that there's incredible secret covered-up-by-the-Deparment-of-Defense physics just waiting to be discovered in these gems."
s "And don't forget that the Department of Defense literally pays people to go around and give talks at MIT to spread misinformation to distract from their UFO secrets!"
hide fenwick
show kublai at right
k "Hey, don't look at me, I'm totally not being paid to promote Kublai: Star Rail!"
s "That's a great example! What do you think Isaac Newton would have said if you had showed him a phone and Kublai: Star Rail, or say, TikTok?"
s "That would have been stunning right? How do you explain that? They didn't know digital logic back then. Addictive algorithms? Had no idea about those."
s "Well, you know where this is going. What's going to be our TikTok?"
s "Are we going to be able to recognize it if it comes along, or are we going to call it a deepfake scam?"
hide kublai
show fenwick at right
f "Look, I know it's important to be curious and keep an open mind, but you're seriously crazy."
s "The data on the internet about this is absolutely overwhelming! You have to look it up yourself!"
f "OK sure, there are probably unexplained phenomena out there, but not New Jersey extraterrestrial handsfree YouTubers."
hide fenwick
show kublai at right with vpunch
k "Actually, I have a mathematical, rigorous proof that UFOs are real!"
k "In fact, I can even prove the existence of New Jersey extraterrestrial handsfree YouTubers, the Riemann hypothesis, and P equals NP!"
hide shl
show gopher at left
g "Oh yeah that Dafny thing you mentioned earlier!"
k "That's right! I'll be happy to share my formal proof written using the Dafny verification language!"
hide gopher
show shl at left
s "Dafny? Ugh, I was trying to teach you Dafny last week and you were too lazy to even solve any of my exercises!"
k "Didn't need to. I'm just too good. Wanna hear my proof?"
hide shl
show gopher at left with vpunch
g "YES! YES! YES!" (screen="shake_say")
k "AAAAAAAAAAAAHHHH!!!"
k "Oh wait, it's just you. You scared me for a sec. Anyways, here we go!"
hide gopher
show lsb at topleft
k "First we define a helper function that computes the largest power of 2 that divides a number."
hide lsb
show sum at topleft
k "And we also need a helper function that sums a sequence."
hide sum
show class at topleft
k "Then we'll create a new class."
hide class
show constructor at topleft
k "And write a constructor for this class that ensures false."
k "Hey, pay attention and read every line! This proof is gonna revolutionize everything!"
hide constructor
show proof at topleft
k "And now we can construct an instance of that class! Assert false! Declare victory!"
stop music
scene black
$ assert False # Click ignore to continue
k "Huh?"
scene bg paper
show kublai at right
show shl at left
with pixellate
play music "deviation2.ogg"
k "Where are we?"
s "Kublai! You fool! You can't prove false is true!"
k "Wait, why not? Dafny said my proof was completely correct and rigorous!"
s "It's probably a Dafny bug! Can't you use some common sense?"
k "Huh, what's wrong with proving false?"
s "Because if false is true then zero is one then zero is any number then zero is my rating for Kublai: Star Rail then any false statement is true!"
show kublai angry
k "WHAT??? You didn't actually rate it zero stars, did you? Is that even possible? I thought the lowest was one?"
s "Anything is possible if you prove false!"
k "Nooo!! You can't deface my beloved Kublai: Star Rail like that!"
k "OK, now I understand why we shouldn't prove false."
k "But did you really leave a trashy rating? Lemme check."
k "No Wi-Fi? What's this nonsense?"
s "We're now trapped in Lethal Logic Land all because you proved false!"
k "NOOOOOO!!! I'll never be able to play Kublai: Star Rail ever again!!"
hide kublai
show fenwick at right
f "Don't panic! Stay calm and let's look around for possible exits."
g "HEEEYYYY! I found something!" (screen="shake_say")
# We're math folks we start level indexing from 1
# Sadly Python is bad so the solution is 0-indexed
# [0, 0]
call level(1, [L(1, 2)]) from _call_level
hide fenwick
show kublai at right
k "What the heck just happened?"
s "Hmmm... I'm not sure either..."
# [0, 0, 0, 0]
call level(2, [L(1, L(2, 3))]) from _call_level_1
k "There's some... pattern going on here."
s "Remember, you can press the back button or PgUp or your mouse scroll wheel to rewind the puzzle!"
s "You can also quick save at the start of the puzzle and then load the save to reset the puzzle."
# [0, 1, 0, 0]
call level(3, [L(1, 2), L(1, L(2, 3))]) from _call_level_2
# [1, 2, 1, 0, 1, 1]
call level(4, [L(1, 1), L(1, 2), A(1, A(2, 3))]) from _call_level_3
play music "strange_inspiration.ogg" fadeout 1.0
k "We did... something!"
k "But I'm pretty confused!"
# [0, 1, 1, 0, 0, 2, 0, 1, 0, 0]
call level(5, [L(1, L(2, 1)), A(2, 1), A(1, A(2, 3))]) from _call_level_4
# [0, 0, 0, 0, 0, 2, 2, 0, 2, 1, 2, 2]
call level(6, [L(1, L(2, A(1, A(2, L(3, 4))))), L(1, L(2, 2)), L(1, L(2, 1))]) from _call_level_5
# [0, 0, 0, 2, 1, 0, 2, 0, 0, 1, 0, 2, 0, 0]
call level(7, [L(1, L(2, 1)), L(1, A(A(A(1, 2), 3), L(4, 5))), L(1, A(1, 1))]) from _call_level_6
# TROLL
call level(8, [L(1, L(2, 1)), L(1, L(2, 2))]) from _call_level_7
play music "nomogus41.ogg" fadeout 1.0
k "Yay!! We're making progress!"
# [0, 1, 1, 0, 0, 1, 0, 2, 2, 1, 0, 1, 1, 0, 1, 2, 1, 1]
call level(9, [L(1, A(1, 1)), L(2, L(1, 2)), A(A(A(A(1, 2), 3), 4), L(5, 6))]) from _call_level_8
# TROLL
call level(10, [1, 2, 3, 4, 5]) from _call_level_9
# [0, 0, 1, 0, 0, 2, 3, 2, 2, 1, 1, 0, 1, 2, 1, 3, 1, 1]
call level(11, [A(1, A(2, A(3, L(4, 5)))), L(2, L(1, 2)), L(3, L(2, 3)), L(4, L(3, 4))]) from _call_level_10
# [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 2, 0, 0]
call level(12, [L(1, L(2, A(3, L(4, L(5, L(6, L(7, 8))))))), L(2, L(3, A(3, 2))), L(1, 1)]) from _call_level_11
play music "nightmarechipheavy3.144.ogg" fadeout 1.0
k "You seem to know what you're doing, but welp I'm still pretty confused..."
# TROLL
# [1, 0, 1, 2, 1, 3, 1, 4, 1, 1]
call level(13, [L(1, 1), L(A(2, A(L(4, 1), L(1, 2))), 3), L(3, A(3, 3)), A(1, 5), L(1, L(3, 3))]) from _call_level_12
# TROLL
call level(69, [A(1, 3), L(5, L(10, 5)), L(1, L(2, 2)), A(9, 11), A(12, 13)]) from _call_level_13
# TROLL
call level(15, [18, 18, 18, 18, 18, 18, 18]) from _call_level_14
# TROLL
# Level 16
call level("this", [1, 1, 1, 1, 1, 1, 19]) from _call_level_15
play music "boundless2.ogg" fadeout 1.0
scene bg bathroom
show shl at left
show kublai at right
with pixellate
s "Wow! We made it! We're back!"
s "Thanks for helping us out!"
g "Awwwww no more puzzles..."
nvl_narrator "{size=69}Credits{/size}"
nvl_narrator "Made using Ren'Py, Krita, Rembg, ImageMagick, and a super buggy lambda calculus library that I wrote."
nvl_narrator "Special thanks to Rustan Leino for creating Dafny and investigating my proof of false!"
nvl_narrator "Music by https://opengameart.org/users/centurionofwar."
nvl_narrator "Inspired by my favorite webcomic, Proof of False, which you can find at proof-of-false.the-user.org on the Wayback Machine."
nvl_narrator "Happy (very belated) birthday Isaac!"
centered "{size=150}And thanks to you for playing!{/size}" (screen="shake_say")
play music "push_ahead.ogg" fadeout 1.0
k "Hey SHL, wanna hear my proof of false again?"
s "Oh no..."
k "What about you over there? Do you wanna hear it?"
menu:
"Nah":
k "Ah man. You're really missing out!"
k "Well have a nice day then. Seeya next time!"
stop music fadeout 2
scene black with fade
$ renpy.quit()
"Sure!":
k "Cool, let's do it!"
s "DON'T YOU DARE-"
hide kublai with moveoutright
k "I'm kidding, I'm kidding, I swear!!"
label secret_ending:
play music "happy_timepass.ogg" fadeout 1.0
s "Hey, completely unrelated question, but do you like poetry?"
jump minigame