Elementary Penguin

@elempeng.bsky.social

493 Followers 232 Following

Elementary Penguin is an okapi at the San Diego Zoo. He likes math and hates food.

Three iridescent Japanese beetles on a leaf.
A cut up pink pineapple in a bowl. It looks like a bowl of pieces of meat.
A red tailed hawk on a tree branch
An old-fashioned amusement park sign that reads “ride the thunderbolt” it appears to be a cloud with a lightning bolt through it
a Lean 4 proof that if f is a coordinate function for the line A B such that f(A) = 0 and f(B) > 0, then the ray AB = {P on line A B : f(P) >= 0}. there is a blue checkmark next to the following code: theorem ray_from_cf (A B : Point) (hAB : A ≠ B) (l : Line) (hAl : A ∈ l) (hBl : B ∈ l) (cf : CoordFn l) (hfA_zero : cf.fn A = 0) (hfB_pos : cf.fn B > 0) : Ray A B = {P | P ∈ l ∧ cf.fn P ≥ 0} := by ext X simp constructor · intro h have hXl := on_line_of_on_ray l hAl hBl h refine ⟨hXl, ?_⟩ rcases h with ha | ha · rcases ha with hb | hb · rcases hb with hc | hc all_goals subst hc; linarith · have ⟨hleft, hright⟩ := btwn_points_mp l A B X hAl hBl hXl cf (hfA_zero ▸ hfB_pos) hb linarith · obtain ⟨hAB, hAX, hBX, hdist, hcol⟩ := ha rcases lt_or_gt_of_ne (mt (cf.injOn A X hAl hXl) hAX) with hb | hb · linarith · exfalso rw [d_symm A B, d_symm B X, d_symm A X, add_comm] at hdist have ⟨hleft, hright⟩ := btwn_points_mp l X A B hXl hAl hBl cf hb ⟨hBX.symm, hAX.symm, hAB.symm, hdist, collinear_symm hcol⟩ linarith · intro ⟨hXl, hfX_nonneg ⟩ rw [le_iff_lt_or_eq] at hfX_nonneg unfold Ray unfold Sgmt simp rcases hfX_nonneg with h | h · rw [hfA_zero.symm] at h have hAX := mt (congrArg cf.fn) (ne_of_lt h) rcases lt_trichotomy (cf.fn X) (cf.fn B) with ha | ha | ha · have hBX := Ne.symm (mt (congrArg cf.fn) (ne_of_lt ha)) have hAXB := btwn_points_mpr l A X B hAX hBX hAl hXl hBl cf h ha; tauto · have hXB := cf.injOn B X hBl hXl ha.symm; tauto · have hBX := Ne.symm (mt (congrArg cf.fn) (ne_of_lt ha)) have hABX := btwn_points_mpr l A B X hAB hBX hAl hBl hXl cf (hfA_zero ▸ hfB_pos) ha; tauto · have hXA := cf.injOn A X hAl hXl (hfA_zero ▸ h); tauto a message on the right says "Goals accomplished!"
A black and white picture of a line of people in front of an ice cream stand. A two story house and a forest are behind the stand.
A picture of a wildfire smoke filled sky above trees. Everything looks yellow
A jigsaw puzzle showing Totoro, Satsuki and Mei sitting on a branch. The moon is above them in the sky.
A jigsaw puzzle showing Totoro, Satsuki and Mei
A figurine made out of red pipe cleaners with a paper head and a massive hand made from a black latex glove. The hand is the size of the rest of the figurine. The face is walleyed, and wearing a top hat.
A hole in the ground filled with baby rabbits
A child’s drawing of two astronauts in space looking at a huge snake that encircles the earth. The first astronaut says, “What?” and the second replies, “Just like it’s always been.” Below the picture is the caption: Well ya don’t see that every day!
A bunch of Lean 4 code that gives an intuitionistic proof of ¬¬(¬¬A → A): example (A : Prop) : ¬ (¬ (¬(¬A) → A)) := fun h => h (fun h2 => False.elim (h2 (fun h3 => h (fun _ => h3))))
Rabbit
Trees reflected in water. The image is almost perfectly symmetrical through the center
A three panel cartoon A man is riding a bike. He puts a stick in the front wheel. He is lying on the ground clutching his knee. The bike is on the ground behind him.
An orange day lily
A young girl lying on a couch with a tan puppy lying upside down on her chest. They are both making pitiful faces
Lady’s Glove. Purple bell shaped flowers, covered in rain drops.
The Space X stock ticker over the last six trading days. Showing an initial spike to over 210 per share before crashing to a current price of about 153 per share.
A large agricultural building on a grassy hill with white clouds above
Colorful birdhouses hanging from the branches of a tree
Two sheep standing next to a roofed wooded structure. A red shed is in the background.
A public playground. A sign on it reads Play It Safe. A girl in overall shorts is walking towards it.
A cemetery. There is a row of small headstones going diagonally from front left to back right. At the head of this row is a larger headstone with an American flag attached to it.
A black and white picture of a dark cloud against a background of white wispy clouds
A dark cloud against a blue sky filled with wispy white clouds
Grey ominous clouds above trees and a backyard. There is a chicken coop in the bottom left of the image
A black-and-white picture of the top of a dead tree
The silhouette of a child on a swing against a clear sky
A Google street view car. A sedan with a giant omnidirectional camera on top.
A bunny hiding behind clover and grass
A plane in a deep blue sky, with twin contrails behind it
a much better picture of the baby rabbit, partially obscured by tall grass.
The same baby rabbit but much closer
A young rabbit standing in clover
A tufted titmouse standing on a leafy twig
A very tiny hamster (roughly the size of a cotton ball) going sickass in her enclosure
A brush pen drawing of pine trees
A black-and-white picture of water plants rising out of a pond. The plants are tear shaped leaves at top stems sticking out of rippling water.
A short cartoon video of a man eating a hotdog, and then eating another person
A bunny in tall grass, eating clover
A screenshot of the Lean 4 playground showing me wasting a ton of time proving baby logic results using type theory
A stereographic representation of elliptic geometry, showing that here the angle sum of a triangle is always more than 180 degrees
A young bird standing between two boughs of a tree
An older man in a black suit sitting next to an older woman with short hair in a Tiffany blue outfit
A close up photo of a cricket on a piece of wood
A ton of geese eating grass near bleachers in a park
A three panel cartoon showing a man on fire using the stop/drop/roll method of dealing with being on fire
A bird standing on the edge of a building’s roof
A teenager and a young girl eating dippin dots
A picture of a woman, a teenager and a young girl riding a teacup carnival ride
A Spotify screenshot showing a playlist called Mr Hat’s Awesome Birthday Mix! With a bunch of emojis
An amusement park ride. People sit in benches suspended from long chains attached to the top of a very tall tower. Clouds are visible in the background.
Me but now wearing a slightly more stylish Barbour bucket hat, without a chin strap.
A picture of me looking like a complete idiot. I’m wearing a wrinkled orange and white aloha shirt and a bucket hat with a chin strap that looks like it’s been lying at the bottom of a drawer crumbled into a ball (because it has).
A screenshot of a conversation with the LLM Claude How many days of the week have a fish in them? Three: TUNAday, FRIday (fry... close enough? Actually that's a stretch), and SALMONday. Wait, let me be honest - just one that's a clean answer: TUNAday (Tuesday). G Lmao that rocks. (This is the latest hallucination from one of your competitors, it says some craziness about the letters FISH being in one of the day names) Ha! That's a great hallucination. To be fair, none of the days of the week contain the letters F-I-S-H in sequence... so whoever that model is, it's truly swimming upstream on that one. Booooo
a very old mickey mouse clock with a green metal case. Mickey doesn't look quite right to the modern eye.
a black and white picture of white circular lights as seen through a piece of plexiglass. Four of the circles align with a figure that resembles the Southern Cross constellation