No toż samo piszę. Zwłaszcza w praktycznych. Jak w szkole nie pamiętałem jakiegoś twierdzenia to kombinowałem z kilku liczb jakie ono jest - nie bawiłem się w dowód ogólny, którego zresztą nie umiałbym przeprowadzić a może nawet nie miałem nawet przebłysku świadomości, że takowy może w ogólności istnieć. Zgarniałem piąchę bez wkuwania i miałem w nosie jak się to ma do platońskiego wzorca. Przypuszczam, że pomarańczowy cymbał i paru innych mogących wciskać guziki kombinuje mniej więcej tak samo. Jak można wyczytać :
Coraz więcej matematycznych dowodów powstaje w języku Lean. To specjalny język i system komputerowy służący do formalnego sprawdzania dowodów. Zwykły matematyk opisuje swoje rozumowanie słowami i wzorami. W Lean trzeba zapisać je jako ciąg precyzyjnych kroków logicznych, które komputer może skontrolować jeden po drugim.
Ja mam na to za mały rozumek, ale tak w ogóle to przypuszczam, że za rogiem czai się Godel.
Poza tym jeśli jesteś w stanie przepisać swoje równanie na ciąg znaków zrozumiałych dla komputera to on sprawdzi, czy gdzieś nie zamieniłeś plusa z minusem czy alternatywy z koniunkcją. Ale jak się rypniesz to sprawdzi co innego - vide z art.:
... firma z wielką pompą ogłosiła rozwiązanie jednego z siedmiu problemów milenijnych, dotyczącego równań Naviera–Stokesa opisujących ruch cieczy i gazów. Matematycy od ponad dwóch stuleci nie potrafili rozstrzygnąć, czy w trójwymiarowym przepływie mogą powstać osobliwości, czyli miejsca, w których matematyczny opis ruchu płynu się załamuje... OpenAI przedstawiła dowód, że w pewnych warunkach takie osobliwości rzeczywiście mogą się pojawić.... trzech matematyków z King's College London i Cambridge opublikowało analizę, w której wskazali rozbieżności między obiema wersjami. Okazuje się, że w kilku miejscach komputer sprawdzał nieco inne twierdzenia niż te przedstawione w tekście dla ludzi.
