INTUITION
Vad är det du ser?
Kvadraten på den längsta sidan har samma area som de två mindre tillsammans. Det är den räta vinkeln som gör likheten möjlig.
Matematisk referens ↗21 UPPTÄCKTER / MATEMATIK & FYSIK
Math Atlas.
Från talens mönster
till kvantvärldens vågor
och rummets geometri.
Geometri / 01
Tre kvadrater. En likhet.
a²
b²
c²
c
Ändra kateterna och se hur kvadraternas areor följer med. Triangeln förblir rätvinklig.
MATEMATIK
Figuren använder flyttal. Lean-beviset gäller den exakta algebraiska identiteten för Pythagoreiska tripplar, inte pixlarna på skärmen.
✓Kontrollerat med Lean 4Euclides formel för heltalstripplar
Figuren använder flyttal. Lean-beviset gäller den exakta algebraiska identiteten för Pythagoreiska tripplar, inte pixlarna på skärmen.
import Std
namespace MathAtlas
theorem pythagoras (m n : Int) :
(m*m - n*n)^2 + (2*m*n)^2 = (m*m + n*n)^2 := by
grind
end MathAtlas
Lean (version 4.33.1, arm64-apple-darwin24.6.0, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
Källfilens SHA-256: 4bf118c476fec7a3bdbc8a5e997c4eb8bd8bbee84d1981f67be0bd52b906e954
LEAN / VAD ETT BEVIS BETYDER
En vacker bild är inte ett bevis.
Lean kontrollerar matematiska påståenden. Webbläsaren ritar konkreta exempel. Ett bevis av en algebraisk identitet bevisar inte att en fysikalisk teori stämmer med naturen, eller att grafik och simuleringens kod är formellt verifierade.
Kontrollerade med Lean 4.33.1 och standardbiblioteket vid bygget. Källfil, versionsnummer och axiomlista finns öppet. Inga ofärdiga bevis eller ersättningsaxiom används.
Reglagen styr JavaScript, SVG och WebGL2. Lean körs inte vid varje bildruta eller när du byter tal. De kontrollerade satserna och exemplen anges separat under varje demo.
Kvant- och relativitetsdemos använder förenklade analytiska modeller. Strängar och kompakta dimensioner är tydligt märkta som klassisk modell eller teoretisk illustration. Ingen experimentell verifiering av strängteori påstås.