Luaigh an t-éileamh. Déanann an eithne cinneadh an bhfuil sé cruthaithe.

Ionsaíonn painéal samhlacha do fhadhb leis an litríocht, SageMath, PARI/GP agus réiteach SMT, ansin foirmíonn an toradh i Lean 4 i gcoinne Mathlib. Glacann eithne Lean leis an cruthúnas nó ní dhéanann sé, agus ní athraíonn aon mhéid próis muiníneach sin. Nuair a theipeann air faigheann tú an sprioc cruinn atá fágtha, agus is gnách go raibh an argóint neamhfhoirmiúil ag waving láimhe.

An sprioc

Bí sonrach faoi cad a chiallaíonn déanta. 'Cinneadh a dhéanamh an bhfuil X fíor, agus a chruthú go bhfuil sé' buille 'inis dom faoi X'.

An barra a bhfuil sé a ghlanadh

Saineolaí cúramach

Cad a ghlacfadh gairmí inniúil sa réimse mar a rinneadh agus ceart.

Caighdeán foilsithe

Bheadh maireachtáil athbhreithniú piaraí: gach éileamh foinse nó díorthaithe, modhanna luaite, …

Cruthúnas foirmiúil

Argóint deductive iomlán. Gach céim údar maith, gach toimhde a luaitear, aon achomharc a dhéana…

Caighdeán duaise

An barra a bheadh ag aighneacht Dhuais Clay Millennium: cruthúnas iomlán, féin-chomhdhéanta, sa…

Grád Cinnidh

Fianaise go leor chun gníomhú ar bhealach tráchtála: roghanna costas, rioscaí ainmnithe, moladh…

Scríobh mo chuid féin

Describe your own standard.

Iarr ar chruthúnas ar leibhéal duais agus inseoidh sé duit go soiléir nuair a thiteann an painéal gearr, seachas bua a dhearbhú.

An painéal

Ciallaíonn suíocháin níos mó uillinneacha níos mó, agus costas níos mó in aghaidh an bhabhta.

Réiteoir

Rialacha ar na critéir agus ath-seiceálacha gach píosa fianaise. Fiú do mhúnla is láidre.

Babhtaí

Teorainn chaiteachais

Má bhuaileann tú é, cuirfidh sé an cluiche ar shos. Níl aon rud caillte.

Infheictheacht

Foilsigh nuair atá sé críochnaithe

Cláraigh chun cluiche a thosú

Cuntais nua a fháil ag tosú creidmheasa, go leor le haghaidh cluiche fíor.

Seiceálaí nach féidir a chur ina luí air

Lean 4 le Mathlib cineál-seiceálacha an ráiteas deiridh, agus cruthúnas a leanings ar sorry, native_decide nó axiom úr a dhiúltú seachas a chomhaireamh.Taobh leis: SageMath, PARI/GP, Z3, CVC5 agus an OEIS, ionas gur féidir le tógáil a ríomh agus a aithint sula ndéanann duine ar bith iarracht rud ar bith a chruthú faoi.

Is fianaise é cruthúnas teipthe

Nuair a theipeann ar fhoirmiú, tugtar an sprioc nach bhféadfadh Lean a dhúnadh ar láimh don suíochán is fearr chun ionsaí a dhéanamh air: ach an sprioc sin, ní an stair ar fad.Ainmníonn cruthúnas diúltaithe an bhearna go beacht, rud atá níos mó ná an chuid is mó argóintí neamhfhoirmiúla a dhéanamh riamh.

Ní chruthaítear aon rud faoi dhó

Téann gach lemma a bhunaíonn an painéal i mórleabhar comhroinnte lena chruthúnas, mar sin ní dhéantar é a athdhíorthú agus ní dhéantar iarracht ar chríocha marbh. Fadhbanna fada sos agus a atosú gan obair a chailleadh: dún an cluaisín agus teacht ar ais amárach.