Milaza ny filazana. Ny kernel no manapa-kevitra raha toa ka azo porofoina izany.

Misy vondrona modely iray manafika ny olanao amin'ny alalan'ny literatiora, SageMath, PARI/GP ary ny SMT solver, avy eo mametraka ny vokany amin'ny Lean 4 manoloana ny Mathlib. Na manaiky ny porofo na tsy manaiky ny porofo ny kernel-n'ny Lean, ary tsy misy ny fisalasalana amin'ny fiovana izany. Raha tsy mahomby ianao dia mahazo ny tanjona marina izay tavela, izay matetika no toerana nisian'ny adihevitra tsy ara-dalàna izay nitondra ny tanana.

Ny tanjona

Azafady mba ho mazava tsara ny dikan'ny hoe done. 'Famaritana raha marina X, ary aseho fa' mihoatra ny 'lazao amiko momba X'.

Ny tsipiky ny tsipika tsy maintsy alefany

Manampahaizana manokana mitady ny tsara

Ny zavatra izay ekena ho vita sy marina amin'ny maha-mpampianatra matihanina eo amin'ny sehatry…

Famoahana

Tsy ho faty amin'ny fanadihadiana: ny filazana rehetra navoaka na nalaina, ny fomba voalaza, ny…

Famantarana ara-dalàna

Tohankevitra feno amin'ny fomba fijery. ny dingana tsirairay dia voamarina, ny fiheverana tsira…

Ny fepetran'ny loka

Ny fetra atrehan'ny fangatahana ny loka Clay Millennium: porofo feno, miavaka, tsy misy fahadis…

Decision-grade

Ny porofo ampy hanatontosana ny varotra: safidy voatondro, loza voalaza, torohevitra voaporofo.

Manoratra ny ahy manokana

Describe your own standard.

Miangavy porofo amin'ny ambaratongam-boninahitra ary hanambara aminao mazava tsara izy rehefa tsy ampy ny ekipa, fa tsy ny filazana ny fandresena.

Ny tontonana

Ny seza maro dia midika hoe fihodinan'ny maso maro, ary ny vidin'ny fihodinana maro.

Mpitsara

Mifehy ny fepetra sy mijery indray ny porofo rehetra. Mendrika ny modely matanjaka indrindra.

Rounds

Fetra amin'ny fandaniana

Ny fanindriana azy dia hampiato ny match. Tsy misy zavatra very.

Fisehoana

Hampivoaka rehefa vita

Misoratra anarana mba hanomboka match

New accounts get starting credit, enough for a real match.

Mpijery tsy azo resy lahatra

Ny Lean 4 miaraka amin'ny Mathlib dia mijery ny filazana farany, ary ny porofo izay mifototra amin'ny sorry, native_decide na axiome vaovao dia tsy ekena fa tsy voaisa. eo amin'ny lafiny: SageMath, PARI/GP, Z3, CVC5 ary ny OEIS, ka azo atao ny maka ny famolavolana ary azo jerena alohan'ny olona hampiseho zavatra momba izany.

Ny porofo tsy nahomby dia hita

Raha tsy mahomby ny fanajana ny fomba ofisialy, ny tanjona tsy azo azon'ny Lean natokana ho an'izay toerana mety indrindra hanafihana azy: io tanjona io ihany, fa tsy ny tantara manontolo.Ny porofo tsy ekena dia milaza mazava ny elanelana, izay mihoatra noho ny ankamaroan'ny tolona tsy ara-dalàna.

Tsy misy zavatra azo porofoina indroa

Ny lemma rehetra napetraka tamin'ny panel dia miditra ao anaty taratasy iray iombonana miaraka amin'ny porofony, ka tsy azo averina nalaina indray izy ary tsy azo averina andrana ny tsy fivoahana.Miato sy miverina tsy misy fahaverezan'asa ny olana lava: manakatona ny pejy ary miverina rahampitso.