Linkblog/2025/03/18
Proofs with Lean, PlayStation Boot Logo is 3D, SM64 without the Z-Buffer.
Today is a YouTube heavy day.
MathPom - Introductory Proof with Lean 4 - Natural Numbers
I’ve heard mention of Lean from certain circles as of late, specifically Dan Abramov.
It was him who posted about this video.
The opening of this video about it was enough to hook me for a bit, but then the latter bit flew right over my head.
But I can’t not put it here, the channel has way too little subscribers, need to pump this content!
Jimmy Breck-McKye - Hacking the PlayStation Boot Logo
The PS1 boot logo is a 3D model!
Its similar to the pop.lmp
file in Quake, in the way that the system will validate that the data contained on the CD is the same value as / matches the hash of something on the system, but the value / data itself is copyrighted, so the idea was (at least at the time in the late 90s), since the system (or in the case of Quake, the game) would not boot without the required data, if a bootleg / copy / rip was created, by it simply having this copyrighted thing inside, would be the thing they would get you on from a legal perspective.
I believe this has since been basically proven not legally binding, but it seems like this was commonplace back in the day.
Fireflake - Super Mario 64 but I Removed the Z Buffer
The N64 was a console that didn’t require sorting your polygons before giving them to the GPU, it has a hardware-based approach to Z-buffering.
Fireflake though, figured out a way to remove that Z-Buffer, and leave the game as is.
It runs just fine, but it a much more visually ‘interesting’ experience.