Changes

7 changed files (+305/-310)

• images/fenwick.webp
• images/kublai.webp
• lambcalc.py
  • @@ -1,139 +1,10 @@
    - import random - from typing import Any, NamedTuple - - - # TODO Move this to other file or something - # Or make it more programmatic - animals = """🐒 - 🦍 - 🦧 - 🐶 - 🐕 - 🦮 - 🐕‍🦺 - 🐩 - 🐺 - 🦊 - 🦝 - 🐱 - 🐈 - 🐈‍⬛ - 🦁 - 🐯 - 🐅 - 🐆 - 🐴 - 🫎 - 🫏 - 🐎 - 🦄 - 🦓 - 🦌 - 🦬 - 🐮 - 🐂 - 🐃 - 🐄 - 🐷 - 🐖 - 🐗 - 🐏 - 🐑 - 🐐 - 🐪 - 🐫 - 🦙 - 🦒 - 🐘 - 🦣 - 🦏 - 🦛 - 🐭 - 🐁 - 🐀 - 🐹 - 🐰 - 🐇 - 🐿️ - 🦫 - 🦔 - 🦇 - 🐻 - 🐻‍❄️ - 🐨 - 🐼 - 🦥 - 🦦 - 🦨 - 🦘 - 🦡 - 🦃 - 🐔 - 🐓 - 🐤 - 🐦 - 🐧 - 🕊️ - 🕊 - 🦅 - 🦆 - 🦢 - 🦉 - 🦤 - 🪶 - 🦩 - 🦚 - 🦜 - 🪽 - 🐦‍⬛ - 🪿 - 🐦‍🔥 - 🐸 - 🐊 - 🐢 - 🦎 - 🐍 - 🐲 - 🐉 - 🦕 - 🦖 - 🐳 - 🐋 - 🐬 - 🦭 - 🐟 - 🐠 - 🐡 - 🦈 - 🐙 - 🐚 - 🪸 - 🪼 - 🦀 - 🦞 - 🦐 - 🦑 - 🦪 - 🐌 - 🦋 - 🐛 - 🐜 - 🐝 - 🪲 - 🐞 - 🦗 - 🪳 - 🕷️ - 🦂 - 🦟 - 🪰 - 🪱 - 🦠""".split() + # Ren'Py uses Python 3.9 + from random import randrange + from typing import Any, NamedTuple - - # Lambda term + ## Lambda term class L(NamedTuple): var: int body: Any
  • @@ -146,70 +17,90 @@ arg: Any
    # Recursively substitute var with rep in term - def sub(term, var: int, rep): - match term: - case L(): - # Replace newly bound variable in rep using alpha conversion - # TODO: Make this even larger so name collisions never happen, or just use a var that isn't used? - # Have some global next unused var or something - var2 = random.randrange(10000000) - return L(var2, sub(sub(term.body, term.var, var2), var, rep)) - # return L(term.var, sub(term.body, var, sub(rep, term.var, var2))) - case A(): - return A(sub(term.fn, var, rep), sub(term.arg, var, rep)) - case int(): - if term == var: - return rep - return term + def sub(term, var, rep): + if type(term) is L: + # Shadowing should never happen + assert term.var != var + return L(term.var, sub(term.body, var, rep)) + if type(term) is A: + return A(sub(term.fn, var, rep), sub(term.arg, var, rep)) + if term == var: + return rep + return term + + + # Add offset to all bound vars + def alpha(term, offset, bound): + if type(term) is L: + return L(term.var + offset, alpha(term.body, offset, bound | {term.var})) + if type(term) is A: + return A(alpha(term.fn, offset, bound), alpha(term.arg, offset, bound)) + if term in bound: + return term + offset + return term # Simplify term using beta reduction def red(term): - match term: - case L(): - return L(term.var, red(term.body)) - case A(): - fn = red(term.fn) - if type(fn) is L: - return red(sub(fn.body, fn.var, term.arg)) - return A(fn, red(term.arg)) - case int(): - return term + if type(term) is L: + return L(term.var, red(term.body)) + if type(term) is A: + fn = red(term.fn) + if type(fn) is L: + # Rename bound vars in fn.body to avoid name collisions + return red(sub(alpha(fn.body, randrange(10**8), set()), fn.var, term.arg)) + return A(fn, red(term.arg)) + return term - # Check equality - # Inputs must be reduced - # TODO: bound vars should still match though??? - # DON'T MUTATE boundvars - # https://stackoverflow.com/questions/26320899/why-is-the-empty-dictionary-a-dangerous-default-value-in-python - def eq(term1, term2, boundvars={}): - if type(term1) != type(term2): - return False - if type(term1) is L: - if term1.var in boundvars and boundvars[term1.var] != term2.var: - return False - return eq(term1.body, term2.body, boundvars | {term1.var: term2.var}) - if type(term1) is A: - return eq(term1.fn, term2.fn, boundvars) and eq( - term1.arg, term2.arg, boundvars + # Rename vars using first available int + # Input term must be reduced first + def canonicalize(term, bound, free): + if type(term) is L: + # Shadowing should never happen + assert not term.var in bound + if len(bound) == 0 and len(free) == 0: + var2 = 0 + else: + var2 = max((bound | free).values()) + 1 + return L(var2, canonicalize(term.body, bound | {term.var: var2}, free)) + if type(term) is A: + return A( + canonicalize(term.fn, bound, free), canonicalize(term.arg, bound, free) ) - if term1 in boundvars and boundvars[term1] != term2: - return False - # Free var - return True + if term in bound: + return bound[term] + if len(bound) == 0 and len(free) == 0: + free[term] = 0 + elif not term in free: + free[term] = max((bound | free).values()) + 1 + return free[term] - # Get friendly uncurried repr of term - def animal_repr(term) -> str: + # Check equality + def eq(term1, term2): + return canonicalize(term1, {}, {}) == canonicalize(term2, {}, {}) + + + animals = "🦊🐱🐸🐷🐼🐶🐭🐻🐨🐯🐺🦁🐮🐹🐰🦝" + + + # Get friendly uncurried repr of canon term + def animal_repr_canon(term): if type(term) is L: if type(term.body) is L: - return f"{animals[term.var]}{animal_repr(term.body)}" - return f"{animals[term.var]}>{animal_repr(term.body)}|" + return f"{animals[term.var]}{animal_repr_canon(term.body)}" + return f"{animals[term.var]}->{animal_repr_canon(term.body)}|" if type(term) is A: - return f"{animal_repr(term.fn)}({animal_repr(term.arg)})" + return f"{animal_repr_canon(term.fn)}({animal_repr_canon(term.arg)})" return animals[term] + # Wrapper func + def animal_repr(term): + return animal_repr_canon(canonicalize(term, {}, {})) + + # https://en.wikipedia.org/wiki/SKI_combinator_calculus I = L(1, 1) K = L(1, L(2, 1))
  • @@ -218,23 +109,54 @@ # https://en.wikipedia.org/wiki/Fixed-point_combinator
    # red(Y) doesn't terminate though... Y = L(1, A(L(2, A(1, A(2, 2))), L(2, A(1, A(2, 2))))) Z = L(1, A(L(2, A(1, L(3, A(A(2, 2), 3)))), L(2, A(1, L(3, A(A(2, 2), 3)))))) + + # Tests assert eq(red(A(A(A(S, K), I), A(A(K, I), S))), I) assert eq(red(A(A(A(S, K), S), K)), K) assert eq(red(A(A(A(S, K), I), K)), K) assert eq(red(A(A(K, S), A(I, A(A(A(S, K), S), I)))), S) - # # eta reduction + # eta reduction assert eq(red(L(1, A(L(2, A(2, 2)), 1))), L(1, A(1, 1))) - - # animal_repr(red(A(A(I, S), A(I, A(A(A(K, K), K), S))))) # Rename bound variable in lambda after name collision assert eq(red(A(K, K)), L(1, L(2, L(3, 2)))) - # Avoid name capture of bound variables # https://www.cs.yale.edu/homes/hudak/CS201S08/lambda.pdf assert eq(red(A(L(1, L(2, 1)), 2)), L(2, 3)) - - # red(A(L(1, A(2, 1)), 2)) should be A(2, 3)?? or A(2, 2)?? # Should two free vars refer to the same var?? # Like maybe we should just assume all vars are bound above us somewhere - # I think that massively simplifies the code + # I think that massively simplifies the code, since then red doesn't need to track currently bound vars # I should choose the one that makes for better puzzles + assert eq(red(A(L(1, A(2, 1)), 2)), A(2, 2)) + + # Brute force!! + def solve(terms, moves, depth): + cnt = sum(type(i) is int for i in terms) + if cnt == len(terms): + print(moves) + return + if len(terms) - cnt > depth: + # Can only increase cnt by one per turn anyways + return + for i in range(len(terms)): + for j in range(len(terms)): + newterms = terms.copy() + newterms[i] = red(A(terms[i], terms[j])) + solve(newterms, moves + [i, j], depth - 1) + + # Alt solver for if arg gets replaced + def solve2(terms, moves, depth): + cnt = sum(type(i) is int for i in terms) + if cnt == len(terms): + print(moves) + return + if len(terms) - cnt > depth: + # Can only increase cnt by one per turn anyways + return + for i in range(len(terms)): + for j in range(len(terms)): + newterms = terms.copy() + newterms[j] = red(A(terms[i], terms[j])) # THIS LINE IS DIFFERENT + solve2(newterms, moves + [i, j], depth - 1) + + + solve2([L(1, L(2, 1)), L(1, A(1, L(2, 1))), A(1, 2)], [], 8)
• lambcalc.rpy (deleted)
  • @@ -1,41 +0,0 @@
    - init python: - from typing import Any, NamedTuple - - # Lambda term - class L(NamedTuple): - var: int - body: Any - - # Application term - class A(NamedTuple): - fn: Any - arg: Any - - - - - label level(terms): - $ N = len(terms) - label loop: - python: - # https://www.renpy.org/doc/html/statement_equivalents.html - narrator("Select eater") - fn = renpy.display_menu(zip(map(animal_repr, terms), range(N))) - narrator("Select food") - arg = renpy.display_menu(zip(map(animal_repr, terms), range(N))) - terms[fn] = red(A(terms[fn], terms[arg])) - if not all(type(i) is int for i in terms): - renpy.jump("loop") - narrator("Level cleared!") - renpy.display_menu(zip(map(animal_repr, terms), range(N))) - - label start: - $ level([L(0, 1)]) - - python: - def f(i): - match i: - case 2: - return 2 - case _: - return 6
• lambcalc.rpyc (deleted)
• script.rpy
  • @@ -1,14 +1,35 @@
    - define k = Character("Kublai", color="#A8836B") + init python: + from lambcalc import * + + # https://www.renpy.org/doc/html/save_load_rollback.html + # terms is a Ren'Py list with rollback capabilities + label level(id, terms): + $ N = len(terms) + narrator "Level [id]" + while not all(type(i) is int for i in terms): + # https://www.renpy.org/doc/html/statement_equivalents.html + narrator "Select food" (interact=False) + # TODO: nothing shows up??? + $ fn = renpy.display_menu(list(zip(map(animal_repr, terms), range(N)))) + narrator "Select eater" (interact=False) + $ arg = renpy.display_menu(list(zip(map(animal_repr, terms), range(N)))) + $ terms[fn] = red(A(terms[fn], terms[arg])) + narrator "Level cleared! Select any option to continue." (interact=False) + $ renpy.display_menu(list(zip(map(animal_repr, terms), range(N)))) + return + + # Chars + define k = Character("Kublai", color="#A8836B") define g = Character("The Go Gopher", color="#E994B2") - define s = Character("Saddam Hussein's LinkedIn", color="#EB4653") + define s = Character("SHL", color="#EB4653") define f = Character("Fenwick", color="#D4CFDB") # Skip the main menu and immediately start the game - label start2: + label start: scene bg codebase show kublai k "Huh?" - k "Um... what are you doing here?" + k "What are you doing here?" menu: "Uh...":
  • @@ -20,18 +41,20 @@ 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..." + 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!" - # TODO: make background white - scene bg ksr at top with vpunch + scene white + show bg ksr at top with vpunch 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!" - scene bg gi at top + hide bg ksr with dissolve + show bg gi at top with dissolve k "You've heard of Genghis Impact at least, right? I mean like, Genghis did have a pretty big impact." - scene bg ksr at top + hide bg gi + show bg ksr at top with vpunch 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 right with vpunch - show kublai at left + show gopher at left with vpunch + show kublai at right g "KUUUUBLAAAIIIII!!!" 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!"
  • @@ -40,113 +63,204 @@ 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... that's why the homepage is gone?" + 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!" - k "Rewrite it in Rust! Or even better, rewrite it in Dafny!" + 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 the Riemann hypothesis using Dafny!" - g "Sure, of course you did, Kublai." - g "Oh shoot, I just realized we're gonna be late to SHL's talk! Let's get going!" + k "I've even managed to prove that P equals NP using Dafny!" + g "Cool! You'll have to show me your proof sometime!" + g "Wait oh shoot, I just realized we're gonna be late to SHL's talk! Let's get going!" k "No way!" - g "I'll download Kublai: Star Rail if you come with me to this talk!" + 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!" + # TODO: get zoomed out image scene bg bathroom with dissolve - # TODO: might need to flip this - show shl at left - s "Hi everyone! I'm SHL the fox, and welcome to MIT!" - s "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 it is by far the nicest shower in the basement of MIT's CS building!" + 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." + hide kublai s "Anyways, today I'll be talking about the variational derivation of the wave equation using invariance under the Poincaré group." show gopher at right with vpunch g "YAAAAAAAAAAYYYYYY!!!" hide gopher - s "But before we start throwing around equations and tensors, I'd like to tell you a bit about *why* I chose to give this talk," + 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 sadly, 2025 is not exactly a year for, you know, old school continuum applied math." + 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 "They stole our tensors and they stole our thunder!" - s "Well, the truth is that machine learning has really changed the world, how research is being done in applied math, how scams are conducted," + 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." - s "I mean, even I'm doing some machine learning nowadays, since people love it when you add a completely unnecessary neural network to your project." - s "But! I've convinced that it's quite possible that continuum applied math and physics might make a resurgence." + 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!" - s "People didn't know how to understand the energy levels of the hydrogen atom, whether nature was deterministic or probabilistic." + 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?" + 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 "And so it's difficult to see to understand what physics is at the moment, and what people do is very different from what they did back in the days. In particular, 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. It's such an exotic material and so forth events, matter, cosmology. But it's not like an immediate things that you want to understand. Why? Why is that so? - - What does that mean for the future of these fields, I mean, I mean, I don't have to convince you that physics is in big crisis, right? The Nobel Prize was awarded to machine learning! It's not saying just that machine learning is doing is important. It's also saying that there's a problem with business. 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. I don't know. Maybe 4 years ago. - - Let's go back to 2020 and COVID. Maybe I can tell you what happened in my field around 2020. So COVID was March 2020. And where were you back? Were you? Was it a high school? Because many of you guys? Yeah. So from our perspective, from the research perspective it hit us like, it hit all of you from a practical sense, but also got us to think about, what kind of research should we be doing? And it's 1 of those events that is kind of having all of us rethink what we're going to do, and for many of us I can guarantee you for more than half of us broadly in the math physics kind of quantitative research community. There was a moment where everybody wanted to be an epidemiologist. They're all marginally full of time. - - We taught classes about like I taught this class, for instance, 18.C20 back then was remote and and then we we were brave enough to give a problem set about how to predict. You know, infection levels and support. Want to do that? We even get messages from parents telling us, well, I'm so glad you're you know my son or daughter was doing this really important stuff. 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 2021. Nobody wanted to hear about nobody anymore. And this idea they wanted to become an epidemiologist had passed the phases."" - - "Because when future historians look back, they won't remember Shakespeare. They'll remember ChatGPT." - - - So what I'm saying is that we like to be reactive to certain things that happen in society. And do you know, when Gen AI happened and hit the scene, do you remember what year, what month ChatGPT came out? You need to remember that right? Those are among those cataclysmic events that we don't have relativity or quantum to drive what society is doing. But we do have these events. And so that was January 2023. It changed the world forever. We're not going back. So it's very possible in my mind that we'll have more of these events in the in the decades to come. 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. And there's growing evidence that that's the case. And it's not just a matter of looking at experiments from particle accelerators or telescopes, you know, that you're in space and things like that, there might be very accessible phenomena that makes us think that physics is actually grossly incomplete, and among those you have what are called *anomalous phenomena*. - - I want to draw your attention to that just for a minute. This is not my purpose to make a class about data that concerns things that we don't understand physically. But I want you to be aware that there's an enormous amount of data out there about things we don't understand. Like I said. It's not my purpose to tell you where this is coming from, but it's present, it's there, and the data are absolutely overwhelming that there are things like this. I'm talking about phenomena that exist and seem to be under the secrecy of defense departments at the moment. In particular, we know that there are thousands and thousands of observations of aircraft or spacecraft that can become invisible in visible lights or in radar. We know that there are observations of craft that have advanced propulsion without wings or rotors and drones, that so seem to be able to go up and down and sideways in ways that seem to define physics, including accelerations that are completely abnormalous, hundreds of thousands of Gs that are not compatible with what we know in aero astro. - - And see, that's not my job to provide you these states. You can go look them up if you want, and follow these rabbit holes. But there are data that are unequivocal that have been, you know, in the public domain. The Department of Defense says, it's real, and it's unexplained, and that nobody's ever been able to define. This has been around for a long time. - - You have examples of phenomena where you can observe these are lights. That is a very powerful lasers that are pointing in the sky. And this comes from a TV show called Skinwalker Ranch. And then you have beams that are being interrupted and startled again later on. Like this, for instance, you have beams of light that go in the sky, and there's no visible object over there. The beam is interrupted, scattered some form here. So you have incredible electromagnetic anomalies, you know, waves that seem to originate from place where it doesn't seem to be a source optical anomalies. - - You have you have materials that are in the hands of defense scientists, mostly, most of it being classified that we don't have to replicate using modern manufacturing methods that seem to buy explanation. So these things do exist. This is an alloy and an alloy of bismuth and magnesium that seems to be at the atomic level, but is impossible to manufacture in which current techniques that we know. So the info is out there that there's a lot of things that we don't understand, and there is not a common understanding in the public that there's something to do from the scientific point of view. - - Quantity of data goes way up. And we, I tell you, if you want to look this up, you'll find a lot of it. The debunking exists, but it's fairly weak. The trustworthiness of it goes down, because nowadays these people say things are deepfakes. But I am fairly convinced, given the incredible weight of the amount of information that's out there that is high quality that there is new physics to be discovered hidden in some of these of these gems. And a lot of it's been hidden behind defense secrecy since the 1950s. There's a lot of it that's just classified. If you try to dig, it's going to be classified, and you're going to add a lot of pushback. So there's clearly something happening with defense craft that is not part of current physics and should 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?" - And also I'm just going to end by saying that there are things that you cannot ignore that are whistleblower claims in Congressional hearings about. Some of you know about dozens of very senior defense officials come out into the public and claim that there's been for several decades a program crash, retrieval, and reverse engineering of supposedly extraterrestrial craft. This, as I'm saying, is the claim that's being made in this Congressional hearings. So people are coming forward under the penalty of perjury. If they lie and they go ahead and say these things. And so the media doesn't really report on any of this. But it is real. And we can also ask ourselves what the media does. My point is, I want all of you to be curious. - - What do you think Isaac Newton would have said if you had showed him the garage door and a garage door opener. That would have been stunning right? How do you explain that? They didn't know electromagnetism back then. Radio waves had no idea about those. Supposedly you can imagine that the reaction of a scientist in the 1700s space with electromagnetic phenomena would have been to have been absolutely stunned by some of those things. - - Well, you know where where is going to be our garage door opener? Are we going to be able to recognize it if it comes along, or are we going to think this is all deepfake? So I want you to keep an open mind that there is a growing amount of information out there. Not just the trustworthiness of it goes down, but the level of interest of people looking at information goes down. - - A lot of this is treated as entertainment. If you look it up. The people who care about all of this, but they care about it not necessarily as curiosity as things to explain as a scientist, but as entertainment. That's a very big danger. Here will we be able to recognize when there's new physics to be found that these are data that should be the basis for the new theories. We have to keep our mind open to that. And there are people increasingly in science and engineering who are sensitive to that. And you're not going to be, if you just follow with the new times, for instance. - - End of parenthesis. I just want you to be to be open-minded. But also I'm telling this because you're MIT kids. And if one day you go look on Amazon, and somebody sells a device that produces free energy, you know. That will, I mean, let's make, let's have a let's have a thought experiment here. + 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 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." - I just said a thousand G acceleration like, what do you? How do you react to that? You say that's fake. That's not real data. Well, imagine for a minute that that's real data. What's the meaning of that? What's the what's the scientific kind of chain of thought that follows? If you say, this is my data point, and I trust it because there's hundreds and hundreds of observations of that I could show you. If you want. It's not my job. But go take a look. You have a craft. It's here, and it goes up in such a way that the acceleration is like that. You can calculate how much energy is corresponds to that kind of acceleration for a craft that you assume has a certain mass like, you know, even a small thing. We're talking orbs. We're talking New Jersey orbs, right? So things that might be small that might be fairly like a probe of some sort. And it's a mass of on the order of a kilogram. Subjected to this kind of acceleration, you can make a calculation for what kind of energy needs to have come into the propulsion to have given it this kind of acceleration here. These are simple calculations that you can make, and we all believe in conservation of energy and all of that right. And you can find you calculate that it's about the energetic output of all the power plants in the United States for one day for that object to have undergone this level of acceleration. + 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}." - So if you believe the data, there's a big open question in physics right there, how do you explain that so much energy was produced by that little thing to have, except maybe it's an optical effect. I don't know but this is where you start thinking. + show fenwick angry at right + 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 smart 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 "HOORAAAAYYYY!" + 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 - And as scientists, as MIT kids, I invite you to think about of these such things. Why? Because one day, if this is all true, it's going to not only change the world, but people, the world would be looking at you. + 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!" + 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." + hide constructor + show proof at topleft + k "And now we can construct an instance of that class, assert false, and declare victory!" + $ assert False # Click ignore to continue - And like, I said, imagine on Amazon, you go ahead and you're able to buy one of these devices that give you the level of energy I was just telling you about. Maybe it's going to be called 0 point energy something whatever. And then, wait, that device works? Well, what do you think of that? You're the MIT kids. You're going to have to figure that one out. The secret came from from, you know, black defense programs. And somehow it's being commercialized. Well, what do you make of this? You got to be able to explain this, you're the MIT kids. + scene bg paper + k "Huh?" + show kublai at right + show shl at left + with dissolve + k "What are we doing here?" + 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 "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!" + k "You didn't actually rate it zero stars, did you? Hold up, 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!" - So what I'm saying is that we might be entering a decade where some of this will become a preoccupation for many of us, and when that time comes you will want to be a physicist. You will want to be a mathematician. You will want to be ready. Everybody will want to become a quantum physicist or relativity specialist at that point. Like back 4 or 5 years ago, we all wanted to become COVID specialists for about a month. Right? + # We're mathematicians, we start indexing from 1 + call level(1, [L(1, 2)]) - So what's the best way to prepare yourself for when these kinds of puzzles will come your way, well, I guess take 18.300 is something you can do. - """ - # That should be extremely abridged since it's only funny for a bit + call level(2, [L(1, L(2, 3))]) - # the gopher and Fenwick are a bit skeptical, but Kublai says he has a proof that UFOs exist and then he proves false in Dafny and the game crashes and locks the chars into a weird lethal logic land that they have to escape by solving puzzles - $ assert False - scene bg paper - # I guess then the gimmick is that the game crashes a lot intentionally? Or at least if infinite recursion happens it'll crash. Actually we should sparingly use that gimmick and only crash once + k "blah" + k "blah" + k "blah" + k "blah" - # probably make a separate file and label and set the vars for the level and jump in (like the poetry minigame in the tgbgame) #then they return back to the normal site and Kublai asks if they wanna hear the proof again and everyone screams, roll the credits, then show link to the proof of false webcomic and the usual homepage at /home.html - - - - # This ends the game. - - return + # That's the end + # $ renpy.quit()
• script.rpyc