środa, 8 października 2008, 01:24

poka-yoke

Jeśli ktoś jeszcze nie wie, co to poka-yoke, to zaraz wytłumaczę (można też poszukać w guglu). Otóż Japończyk Shigeo Shingo nigdy nie pamiętał, czy wziął już swoją tabletkę nasenną czy nie. Tak się tym denerwował, że czasem w ogóle nie mógł usnąć. Aż w końcu wpadł na pomysł — każdego ranka jedną pastylkę z buteleczki odkładał do specjalnie przygotowanego pudełeczka. Wieczorem zaglądał do pudełeczka. Jeśli tabletki nie było, wiedział że już ją połknął. Jeśli była, to ją łykał. Nareszcie mógł spać spokojnie.

Shingo usprawnił też proces składania budzików w fabryce, w której pracował. Zgodnie z instrukcją robotnik miał włożyć do budzika dwie sprężynki. Ale czasem zapominał o jednej i budzik nie działał jak należy. Shingo wpadł na pomysł, by obie sprężynki kłaść wpierw na tacce. Teraz od razu było widać, gdy ktoś zapomniał włożyć sprężynkę — zostawała na tacce. Tacka nie chroniła przed roztargnieniem, nadal zdarzało się zapomnieć o sprężynce. Ale zapobiegała skutkom pomyłki, pozwalała wadę natychmiast usunąć. Sztuczkę z tacką nazwano poka-yoke, czyli unikanie (yokeru) błędów (poka). Poka-yoke i inne metody dobrej organizacji produkcji sprawiły, że Toyota jest dziś najpopularniejszą marką samochodu na świecie. I nie musi być wcale czarna (sporo nazmyślałem, resztę pokręciłem, ale nic nie szkodzi).

Stereotypowy Japończyk prędzej polegnie w walce z własnymi słabościami niż potrafi się z nimi pogodzić. Jak widać — przynajmniej w pracy — Japończycy nie tylko przyznają się do słabości, ale i znaleźli na nie lekarstwa. A my? My wymyśliliśmy errare humanum est. A poka-yoke uczymy się od Japończyków.

31 komentarzy:

tichy pisze...

dobre
(poza konkluzją, która zaprzecza sama sobie)

kwik pisze...

@ tichy
Starałem się być tak zwięzły i treściwy, że przesadziłem. My oczywiście też odkryliśmy, że człowiek jest omylny i błądzący, ale zamiast uznać fakty i jakoś sprytnie sobie z nimi radzić, nadal postulujemy, żeby błędów nie robić. Mamy naturalną(?) skłonność do zatrzymywania się na etapie prostej konstatacji i słusznych postulatów. A życie sobie. Muszę jeszcze sprawę przemyśleć. Dziękuję.

MEP. pisze...

Wychodzi, jak zwykle, na zloty srodek:)
No bo seppuku z powodu srubki czy sprezynki to tez chyba przesada.
A w Toyocie rzeczywiscie maja hopla na punkcie organizacji pracy. Nad poszczegolnymi etapami pracuja czterosobowe teamy (kazdy moze zastapic kazdego) i te zespoly nie tylko wymieniaja sie zadaniami miedzy soba, ale z czasem zmieniaja "etap", zeby nie wpasc w rutyne i nie zglupiec.
Ale mnie i tak najbardziej podobal sie robocik transportowy (podobny od R2D2:), ktory porusza sie po wyznaczonej trasie i sam do siebie mowi ( to znaczy ostrzega, ze sie zbliza, ale po japonsku brzmi to jak mamrotanie pood nosem - slodkie:)

kwik pisze...

@ MEP.
U nas taki robot transportowy pewnie by strasznie wył i świecił, przeszkadzając wszystkim w pracy. Ale może się mylę.

MEP. pisze...

>kwik
Ale przynajmniej wszyscy by wiedzieli, ze MAMY ROBOTA. Co komu po robocie, ktory nie wyje i nie swieci?

kwik pisze...

@ MEP.
Polski robot pewnie by TYLKO wył i świecił.
Ale przynajmniej jesień mamy piękną.

andsol pisze...

Larum! errare nam pokaru!
"Poka-yoke uczymy się od Japończyków"? Ależ nigdy, za żadną cenę. Wolę polskie błędy w polu.

Europa wymyśliła poka-yoke przed wiekami i nazywało się to "supełkiem". Może i dobrze, że znikło, bo supełki na zasmarkanych chusteczkach nie były zdrowe, a na ligninie supełki są brzydkie. I dlatego potem wymyślono budzik oraz notesik, ale jak ktoś zapomina włożyć sprężynki do budzika albo słowa do notesika, to nie ma rady, po prostu powinien sprawdzić jaki rodzaj sake nie przynosi kaca.

To w ogóle nieporozumienie, bo przykre zapominalstwo nic nie ma wspólnego ze szlachetnym błądzeniem. Błędy są (że tak wyniośle powiem) milowymi kamieniami naszego rozumowania. Siedzę, siedzę i wysiedzę taki kamień, wrzucam go do kosza od śmieci i płodzę następny kamień milowy i tak długo to robię, aż robić to przestaję, bo moje działanie czy rozumowanie staje się bezbłędne. I dlatego, że nasi przodkowie błądzili, wymyślili Stany (tak, dziś chwilami żałujemy, że nie zrobiliśmy tego bez błędów) i dzięki temu admirał Perry popłynął do Japonii i przekonał ich do kupowania naszych budzików i w konsekwencji dziś oni mogą zapominać o sprężynkach w budzikach a nawet mogli by zapomnieć o robieniu tamagotchi. Howgh.

kwik pisze...

@ andsol
Najbardziej błądzę, gdy wydaje mi się, że znam drogę. Zapominalstwo też powoduje błądzenie, choć oczywiście mniej szlachetne niż błądzenie w terenie całkiem nieznanym. Ale w nieznanym terenie możemy najwyżej próbować iść prosto, co też wcale nie musi być dobrym rozwiązaniem.

Tak czy owak krążymy ciągle wokół metafory zgubionej czy pomylonej drogi, rozumowanie jest podróżą, dochodzeniem do prawdy, do wniosku, myśli biegną itp. Ciekawe jak jest w japońskim, może oni nie posługują się tak krępującymi metaforami i dzięki temu czasem potrafią coś wymyślić lepiej od nas. Myślenie jednak nie jest chodzeniem.

Supełki czy notes to nie poka-yoke, bo oderwane są od czynności, którą mają ułatwić czy przypomnieć. Dyskietka ma ścięty róg i narysowaną strzałkę, musisz ją włożyć bezbłędnie bo inaczej się nie da - to jest poka-yoke. Zapisana w notesie instrukcja wkładania dyskietki to jednak nie to samo.

Ciekawe kto pierwszy narysował strzałkę. Albo położył strzałę. To był wielki wynalazca. A czy małpy pokazują coś sobie palcami? Kto wynalazł metodę ostensywną? Pies pointer?

Cyncynat pisze...

poka-yoke & errare humanum est
W produkcji oprogramowania jest wiele idei podobnych do poka-yoke. Poczawszy od defensive programming, poprzez design by contract, do (w pewnym sensie) test driven development. Pewnie quality control z innych dzialek tez mialoby sporo wspolnego. Jesli przelozyc na przyklad sprezynek, defensive programming by wygladalo np tak:
1) wziac dwie sprezynki. pomacac, powachac i dobrze obejrzec. w porzadku: to sa rzeczywiscie sprezynki, a nie np srubki.
2) odlozyc na tacke i policzyc. jedna, dwie - wszystko sie zgadza.
3) przygotowac budzik. zajrzec do niego i upewnic sie, ze w nim nie ma jeszcze sprezynek.
4) wlozyc sprezynki do budzika. natychmiast obejrzec sie i sie upewnic, ze na tacce juz nie ma sprezynek. jeszcze raz zajrzec do budzika i policzyc sprezynki: jedna, dwie.
5) fiu, udalo sie.

techniki takie, jednak, sa dobre do czynnosci o zlozonosci wkladania sprezynek do budzikow.

ciekawostka jest to, ze Japonczycy raczej nie slyna ze swojego oprogramowania (Polacy, zreszta, tez nie).

A odnosnie "errare humanum est". W SE funkcjonuje odpowiednik, powiedzenie, ktore niektorzy okreslaja jako Lubarsky's Law of Cybernetic Entomology: there is always one more bug. To powiedzonko wynikalo z empirii, ale i z teorii tez - przypomina, ze zadne poka-yoke nie jest w stanie wyeliminowac bledow.

andsol pisze...

trafiło
@Kwik: mimo znacznej odporności przeciw uczeniu się nowych rzeczy i mimo przywiązania do swojskich błędów, wyjaśnienie o obciętym rogu dyskietki trafiło do mnie i nie potrafię udawać, że nie rozumiem. Więc mogę tylko wdzięcznie gderać: no dobra, dobra.

Proszę, z mego wpisu wytnij uwagi o chusteczkach i zastąp jakimiś mądrymi myślami, by nie zostawiać dowodów, że się myliłem. Ja błędy lubię _robić_, a nie pokazywać je. I am not an errant exhibitionist.

Idea wykazujących właściwości psa pointera głęboko do mnie przemawia, bo zgadza się ze znanym faktem, że po założeniu konfederacji szwajcarskiej, która przyniosła zanik podatków drogowych i przemytu, bezrobotne owczarki wynalazły owce.

@Cyncynat: przypomniałem sobie, że widziałem już podobny przepis, choć nie było tam mowy o obronnym programowaniu. Myślę o "Instrukcji chodzenia po schodach" Julio Cortazara.

Cyncynat pisze...

andsol
ale w odroznieniu od instrukcji chodzenia, defensive programming ma sporo sensu i jest popularne do dzis.

kwik pisze...

@ Cyncynat
Oprogramowanie jest nadal dość okropne i chyba tylko z przyzwyczajenia się temu nie dziwimy. Domyślam się, że proces tworzenia jest jeszcze straszniejszy. Właściwie to zdumiewające, że programy są nadal ręcznie pisane przez ludzi, literka po literce. Taka technika tworzenia oprogramowania to rzemiosło artystyczne, nie inżynieria. Tutaj się już wiele nie da ulepszyć, nawet jeśli odkryjemy już wszystkie sposoby skutecznego pisania programów, a jeden drugiemu będzie patrzeć na ręce.

kwik pisze...

@ andsol
Mogę najwyżej zamazać korektorem na ekranie albo wyciąć wszystko. Z dwojga złego wybieram trzecie rozwiązanie, niech już zostanie tak jak jest.

Cyncynat pisze...

kwik
ale sie nie dziwisz, ze ksiazki sa pisane nadal przez ludzi, i ze nadal sa, przewaznie, okropne?

oprogramowanie zawsze bedzie pisaniem literka po literce. wynika to z bardzo prostej rzeczy - program jest slowem i ktos musi to slowo napisac - literka po literce. rowniez dowody matematyczne tez beda pisane dokladnie tak samo: literka po literce. z tego samego powodu.

co do postepu i "ulepszania": zludzenie. postep jest calkiem spory, choc bledy nadal sa. wczoraj sie recznie dziurkowalo perfokarty, jakby nie patrzyc.

o tym, ze SE sie rozni od elektroniki i budowania mostow juz dawno temu grube ksiazki napisano, to truizm. sa dwie glowne przyczyny: latwosc modyfikacji (latwiej jest poprawic program niz "poprawic" most) i skala zlozonosci (windows ma setki milionow linii kodu, zaden most, samochod czy processor do tego porownac sie nie moze).

to, ze wzgledna ilosc bledow zostaje postrzegana jako taka sama wynika juz z biznesu. dominujaca filozofia, opisana swojego czasu chyba przez Yourdona, jest tzw Good Enough Software. jakosc mozna poprawiac praktycznie w nieskonczonosc, ale kto za to zaplaci?

wyeliminowac bledow *zupelnie i wszedzie* sie nie da: na ich obrone jest tzw twierdzenie Rice'a, przez ktore nie przeskoczysz. ale gdybysmy sie zatrzymali na tak pesymistycznych kostatacjach jak twierdzenie Rice'a czy twierdzenie Goedla, to nie byloby ani zadnych dowodow matematycznych, ani zadnych programow.

ja poprzednio podalem te najprostsze metody, bo przypominaly poka-yoke, ale sa tez znacznie bardziej wyrafinowane, powiedzmy, sposoby. (ostatnia wielka nadzieje (moja) budza prace Daniela Jacksona z MIT. tzw lightweight formal methods. )

Cyncynat pisze...

btw
oczywiscie porownania z procesorami jest o tyle niedobre, ze procesor jest, w duzej mierze, programem. zatem i weryfikacja procesorow wyglada dosc podobnie do weryfikacji oprogramowania. oczywiscie, wymagania jakosciowe wobec procesora sa zwykle znacznie wyzsze niz wymagania wobec edytora tekstu.

tutaj sa dosc ciekawe papers:
"Validating The Intel® Pentium® 4 Processor"
ftp://download.intel.com/technology/itj/q12001/pdf/art_3.pdf

"Validating the Intel® Pentium® 4 Microprocessor"
http://www2.dac.com/38th/acceptedpapers.nsf/9cfb1ebaaf59043587256a6a00031f78/1466dd0df76c8e1e88256a78006d4cae/$FILE/16_1.PDF


tam mozna wyczytac, ze design Pentium4 to jakis milion linii kodu w Structured RTL. projekt weryfikacji zajal 4 lata dla calkiem sporego zespolu.

sekcje Results sa tez ciekawe.

"Cluster-level testing proved to be a big win, as 3411 of the 5809 bugs found by dynamic testing were caught at the CTE level with the other 2398 being found on the full-chip SRTL model. Code inspection was, as always, a highly effective technique that accounted for 1554 bugs, with the remaining 492 being found by Formal Verification, SRTL-to-schematic equivalence verification, and several other minor categories."

z czego wynika, ze jakies 59% bledow wylazlo podczas testowania (unit testing, mniej wiecej), 27% wylazlo podczas code inspections (czyli uwaznego wgapiania sie w kod), a jakies 8% - z formalnej weryfikacji i takich tam.

Cyncynat pisze...

kurde
moje "wyliczenia" procentowego udzialu bledow wg metody znalezienia sa do dupy.
bylo: 59%, 27% i 8%; a powinno byc: 74%, 20% i 6%.

kwik pisze...

@ Cyncynat
Jeśli jakaś nowa metoda bezbłędnego programowania budzi Twoje wielkie nadzieje, to chyba znaczy, że dotychczasowe metody, nawet jeśli nie są całkiem do dupy, to jednak nie wywołują Twojego entuzjazmu. Dążenie do bezbłędności musi być nudne do porzygania, rzuciłem okiem na "test driven development" i nie wygląda to radośnie. Już pewnie więcej uciechy jest przy usuwaniu błędów. Człowiek najwyraźniej nie jest stworzony do robienia nudnych rzeczy, w tym nieźle wyręczają go maszyny. Programowanie byłoby ciekawsze, gdyby człowiek zajmował się częścią kreatywną, a maszyna (program) robiła resztę. Na razie większość programistów chyba nie ma ciekawej pracy, skoro np. Visual Basic jest trzecim językiem pod względem popularności. Wcale nie śmieję się z VB, bo to mniej więcej pułap moich możliwości, chodzi mi raczej o to, że większość czasu przeciętnego programisty pochłaniają czynności dość bezmyślne. Oczywiście nie wiem co z tym fantem zrobić, gdybym wiedział to pewnie już byłbym bogaty.

Swoją drogą względna łatwość modyfikacji oprogramowania i bezkarność twórców na pewno prowokuje błędy, gdyby programista tak jak inżynier musiał stanąć pod zbudowanym przez siebie mostem to pewnie by się tak nie mylił.

Tak podane statystyki intela niewiele mówią (zaskakuje mnie 20% skuteczność czytania kodu), tu trzeba by znać kolejność wykrywania błędów (pewnie jest to opisane w podanych przez Ciebie linkach, ale nie mam na razie siły tam zajrzeć) . To bardzo budujące, że Intel tak otwarcie pokazuje swoje podszewki. Dla porządku przypomnę, że nie zawsze tak było:
http://en.wikipedia.org/wiki/Pentium_FDIV_bug

kwik pisze...

@ Cyncynat
To zdanie (dotyczące Pentium 4) jest godne podkreślenia:
However, it was clear from the start that we couldn’t formally verify the entire design – that was (and still is) way beyond the state of the art for today’s tools.

Czyli na razie nie można formalnie udowodnić, że procesor się nie myli. Można tylko tak sądzić po jego zachowaniu. Ale jest tu też sugestia, że kiedyś będzie to możliwe.

Cyncynat pisze...

kwik
test driven development: to jedno z obecnie popularnych podejsc. nie jest bardziej nudne niz sprawdzanie tacki ze sprezynkami, na moje oko zdecydowanie mniej nudne.

odpowiedzialnosc programisty. jest to popularne misconception. to nie programista moze sie podpisac pod jakoscia programu, lecz firma, bo to firma jest odpowiedzialna za ustalanie procedur QA i firma ustala budzet. a firma ma na wzgledzie biznes i goof enough software, ktore czasem powinno byc calkiem good, ale czesto wystarczy ze bedzie zupelnie kiepskie. gdyby zrobic programiste realnie *odpowiedzialnym* za jakosc to na kazde proste nawet zadanie zadalby po 20 lat (pelna weryfikacja moze zajac i wiecej, ale po 20 latach mozna poszukac innej pracy). a staniecie pod mostem? no po to jest powtarzalnosc i prostota mostow. a kto polecialby skonstruowana przez siebie rakieta na Mars?

weryfikacja procesora: no ja wyraznie napisalem ze problem formalnej weryfikacji jest *niemozliwy*, zadne toole nie zrobia go mniej niemozliwym. zupelnie tak samo jak problem dowodzenia dowolnych twierzen - nie ma magicznego narzedzia do dowodzenia dowolnych twierdzen. ja pisalem o metodach, ktore pozwola wykryc wiecej bledow, a nie o metodzie, ktora wykryje wszystkie bledy. to moze jest mozliwe przy konstruowaniu bud dla psow czy innych mostow (podobnie jak mozliwe rozwiazywanie rownan kwadratowych), ale nie w przypadku ogolnym. juz pisalem: twierzenie Rice'a.

Cyncynat pisze...

skutecznosc patrzenia
no peer review jest podstawa weryfikacji tekstow naukowych. tyle ze przecietny paper to ma 10 stron (a nie 10 mln stron) i niescislosc w nim nikomu komputera nie zawiesi.

Cyncynat pisze...

statystyki i patrzenie
statystyki tylko potwierdzaja, ze w zdecydowanej wiekszosc i bledy sa banalne. na banalne bledy dobre sa banalne metody, tylko na te kilka procent sa wymagane bardziej wyrafinowane narzedzia.

kwik pisze...

@ Cyncynat
Żeby mieć jasność - tu jest podobny cytat, tym razem kogoś z Motoroli:
"The truth is that formally verifying that the entire design implements the specification is not generally possible today"
http://www.eetimes.com/story/OEG20010621S0080
Tu też jest niedwuznaczna sugestia, że dziś niemożliwe, ale w przyszłości - czemu nie?

Żaden zdrowy na umyśle naukowiec nie uzna, że publikacja jest wiarygodna dlatego tylko, że już ją kilku innych przez grzeczność przeczytało i swoje zdanie wyraziło. Jeśli jest w publikacji coś kontrowersyjnego, to od razu wszyscy się rzucają do sprawdzania wyników. Reakcja na nowy procesor jest jednak inna, raczej prawie pełne zaufanie. A nowe oprogramowanie jednak nie budzi takiego zaufania.

Inżyniera pod mostem przywołałem nie tylko dlatego, że jest humorystyczny, chyba coś w tym jest. Wystarczy przeczytać warunki licencji dowolnego oprogramowania, producent podkreśla, że nie ręczy za nic. Za jakieś podstawowe właściwości chyba mógłby jednak ręczyć, nie ryzykuje przecież więcej niż ten inżynier pod mostem.

Cyncynat pisze...

kwik
"The truth is that formally verifying that the entire design implements the specification is not generally possible today"

i jutro i pojutrze tez. tu nie ma dwoch zdan, to jest zwyczajnie niemozliwe, o tym sie na studiach uczy. to zdanie jest dokladnie takie same co takie: na dzien dzisiejszy nie mamy narzedzi do automatycznego dowodzenia dowolnych twierdzen. czy to prawdziwe zdanie rowniez wzbudziloby w Tobie nadzieje, ze moze jutro sobie z sieci sciagniesz programik ktory Ci szybko udowodni hipoteze Riemanna?

sukcesy czesciowe sa czasami mozliwe. w takim sensie, ze dla pewnych ograniczonych podzbiorow designow i dla pewnych ograniczonych podzbiorow specyfikacji weryfikacja jest mozliwa. te podzbiory nie musza sie pokrywac z niczym praktycznym (i sie nie pokrywaja, zwykle).


a gwarancje? to kwestie biznesu, naprawde. zaplacilbys pare milionow dolcow za konto na S24 z "gwarancja dzialania"? gwarancja bedzie obejmowala tylko najprostsze funkcjonalnosci, a oprogramowanie bedzie gotowe gdzies do 2023 roku; jak dobrze pojdzie. czy jednak wolisz bezplatny, kiepskawo dzialajacy Salon ale na wczoraj? tam gdzie sa biznesowe uzasadnienia gwarancji, owe gwarancje sa.

Cyncynat pisze...

tak sobie pomyslalem
moze ten ktos z Motoroli mowil o tym, ze oni nie maja narzedzi nawet do recznej weryfikacji (w sensie: siedzenie z olowkiem i dowodzenie matematycznych twierdzen)? to by sie tez zgadzalo, nawet to nie jest dostepne na dzis. ale nawet jak beda takie "narzedzia", to ciezar dowodu bedzie na czlowieku, a to nie bedzie w najmniejszym stopniu praktyczne.
ja jednak pisalem o automatycznej weryfikacji, bo tylko to bedzie praktyczne.

Cyncynat pisze...

btw
do prasy "popularnej" na ten temat nie warto zagladac.

5-ty akapit:

"Using formal verification, Bentley said, the Intel team found more than 100 "high-quality" logic bugs that would not have been uncovered any other way. "

"would not have been uncovered any other way"? to przeciez jest nonsens.

kwik pisze...

@ Cyncynat
Miałem uzasadnioną dwójkę na maturze z matematyki, więc hipoteza Riemanna leży nieco poza granicami moich kompetencji. Tu mógłbym rezolutnie dodać - na dziś.

Natomiast ciekaw jestem, czemu ten gość z intela i tak samo ten drugi z Motoroli mówią, jakby sprawdzenie całego procesora było kiedyś możliwe. Symulator gigaherzowego P4 udawał na linuksie z P3 procesor kilkuherzowy, czyli trzy rzędy wielkości wolniejszy. W tym tempie rzeczywiście trudno zdążyć przed końcem świata. Może chodzi im o to, że można zrobić odwrotnie, symulować jakiś prosty procesor na bardzo szybkim komputerze. Wtedy dałoby się go sprawdzić dużo dokładniej.

Popularną prasę jednak łatwiej zrozumieć, albo raczej nabrać złudzenia, że się rozumie.

Cyncynat pisze...

kwik
formalna weryfikacja wlasie polega na tym, ze sie udowadnia, ze program bedzie dzialal zgodnie ze specyfikacja od teraz az do nieskonczonosci.

praktycznie jednak czesto wystarczy pokazac, ze program bedzie dzialal w okolicach zgodnosci ze specyfikacja od teraz az do obiadu. to jest praktyczne i tym sie zajmuje np wspomniany Daniel Jackson. ale to nie nazywa sie "formal verification".

kwik pisze...

@ Cyncynat
Sprawdzanie jak widać niejedno ma imię. Jeśli sprawdzam np. czy mam klucze to sprawdzam raz i tego się trzymam. Czułbym się nieswojo sprawdzający kilka razy. Ale już jakieś proste rachunki na papierze sprawdzam dwa razy. A podejrzaną pamięć w komputerze trzy razy.

Zgaduję, że większość ludzi (tak jak ja) w "na dzień dzisiejszy nie ma" widzi cień nadziei, w odróżnieniu od "nie ma i nie będzie". To co jest formalnie prawdą, praktycznie prawdą nie jest. Ktoś puka do drzwi mojego zmarłego sąsiada i pyta się mnie, czy on tu mieszka, właściwa odpowiedź - "nie nie mieszka". A prawdziwa odpowiedź nawet nie jest odpowiedzią na pytanie.

andsol pisze...

zawracanie głowy, czyli nie na temat
Rzeczesz, Kwiku: "Miałem uzasadnioną dwójkę na maturze z matematyki, więc hipoteza Riemanna leży nieco poza granicami moich kompetencji." Ja też byłem niewiele lepszy i owa hipoteza leży tamże, ale to jest ciekawe, że ludzie oddający jej duże kawałki życia nie zawsze dobrze na tym wychodzą. Jak do tychczas, przynajmniej.

Zacznę od tego, że mój instytutowy kolega Genaldo jest mieszanką wariata i geniusza, z przewagą pierwszego. Gdyby któreś ze swych głupich pomysłów pogłębił, może drugi składnik by przeważył. W każdym razie będąc w miarę młody robił, robił i nie zrobił doktoratu w Stanach, bo miał dziwne poczucie humoru i zabawiał swego promotora antysemickimi dowcipami. Zgadnij z jakiej rodziny był promotor. Potem umarł i jego kolega przyznał, że dowcipy dowcipami, ale teza zasługiwała na tytuł i gdyby Genaldo wrócił, pod nowym przewodnictwem dostałby tytuł. Ale wariat wziął górę i się zaciął. Przy okazji, wymyślał kiedyś klona Unixa, ale odkrył, że niejaki Torvalds właśnie puszcza na usenecie jakieś jajko 0.93 czy 0.94 i odechciało mu się. Tak czy inaczej gdzieś tam poznał De Brandesa, który miał dość otoczenia, nie chcącego uznać, że jego dowód hipotezy Bieberbacha jest poprawny. Genaldo namawiał go na Brazylię i zdaje się niewiele brakowało, byśmy mieli jeszcze większego wariata w instytucie.

Nie pamiętam czy w końcu 2004 czy na początku 2005 dostałem trzy grube pliki De Brandesa z dowodem hipotezy Riemanna oraz skromnym opisem jakie cechy jego umysłu przyniosły ten wspaniały wynik. Nawet zamierzałem zacząć czytać, ale potem sobie przypomniałem, że dowód hipotezy Bieberbacha był sprawdzany przez kupę ludzi z instytutu Stiekłowa przez kupę miesięcy, więc co ja się będę podniecał. Tym bardziej, że to nie moje poletko.

No i do dzisiaj De Brandes myśli, że dowiódł, a inni pytają gdzie dowód, a on pokazuje pliki a inni kręcą nosem. A całkiem niedawno jego były uczeń o niedługim nazwisku Li, utrzymujący od lat, że jego mistrz hipotezy nie dowiódł, wrzucił do arXiv-ów własny dowód, ale po paru dniach stamtąd go usunął. Więc hipoteza nie jest prosta także dla ludzi lepszych na maturze z matematyki. A także pojęcie "dowodu" w matematyce czasami szczerzy do nas zęby w nieprzyjemnym uśmiechu. I ja tam chciałbym skromniej, żeby dowód Halesa + komputera dla hipotezy Keplera został potwierdzony przed (na przykład) olimpiadą z roku 2032 w Tiranie, to już będzie nieźle.

andsol pisze...

to nie klawiatura
Zerknąłem na mój wpis i nie rozumiem czemu De Brangesa systematycznie nazywam De Brandesem. Chciałbym zrzucić winę na klawisz, który się zaciął, ale prawda jest taka, że mózg mi się zacina i oczy zamykają, bo wróciłem z jakiejś tortury gimnastycznej po miesiącach nicnierobienia i myślałem, że mi poskręcało wszystkie kości, ale widzę, że najwięcej ucierpiał mózg.

A w S24 "preview" by nie zaszkodził...

kwik pisze...

@ andsol
Bardzo obszerne ma on hasło w wiki, nic z tego nie rozumiem, ale historia trzyma w napięciu.
http://en.wikipedia.org/wiki/Louis_de_Branges_de_Bourcia

A tu obejrzałem jego zdjęcie w berecie
http://www.math.purdue.edu/~branges/site