Uhakiki
The Lumenary inalenga kuaminika zaidi kuliko nyenzo za kawaida zilizotengenezwa na AI. Ukurasa huu unaripoti hasa kilichokaguliwa, kwa kutumia nini, na kisichokaguliwa.
Uthibitisho rasmi (Lean)
Matamko 88 yamekompailiwa kwa leanprover/lean4:v4.35.0; 0 yanategemea sorry. 3 yanatumia nadharia ya maktaba, 59 yamethibitishwa hapa, 26 ni fasili.
Imetengenezwa 2026-10-28 06:13
Maabara rasmi →Majaribio ya kikokotozi (Python)
Majaribio 12 kati ya 12 yaliendeshwa na kufaulu vipimo vyake. pytest: 571 vimefaulu, 0 vimeshindwa.
Python 3.10.12 · sympy 1.13.3 · mpmath 1.3.0 · numpy 2.2.5 · pytest 8.3.5 · Imetengenezwa 2026-10-28 06:13
Ukaguzi wa maudhui
Ukaguzi wa kiotomatiki 105 umefaulu, 0 umeshindwa (skima, grafu ya masharti ya awali, rejista, tafsiri, uchanganuzi wa majibu).
Ukaguzi kamili kwenye kivinjari (lugha sita, mazoezi, grafu, mazingira salama ya Python): 15 zimefaulu, 0 zimeshindwa.
Imetengenezwa 2026-10-28 06:16
Ukaguzi wa binadamu
| Jaribio | Ushahidi | Hali |
|---|---|---|
| Cantor's diagonal trick on a finite list | Ukokotoaji kamili | imefaulu |
| Clock arithmetic: which residues have inverses? | Ukaguzi kamili wa visa vyote vyenye kikomo, Ukokotoaji kamili | imefaulu |
| Sorting and counting a market basket | Ukokotoaji kamili, Ukaguzi kamili wa visa vyote vyenye kikomo | imefaulu |
| Composing functions: associative, but order matters | Ukaguzi kamili wa visa vyote vyenye kikomo, Mfano kinzani | imefaulu |
| Counting functions, injections and surjections | Ukaguzi kamili wa visa vyote vyenye kikomo, Ukokotoaji kamili | imefaulu |
| Forty primes in a row, then a counterexample | Ushahidi wa majaribio, Mfano kinzani | imefaulu |
| Exact versus numerical: 0.1 + 0.2 and the square root of 2 | Ukadiriaji wa kinamba, Ukokotoaji kamili, Ukokotoaji wa kiishara | imefaulu |
| Hunting for inverses in the integers and the rationals | Ushahidi wa majaribio, Ukokotoaji kamili | imefaulu |
| Does a random walk come home? Statistical evidence | Ushahidi wa kitakwimu, Ukokotoaji kamili | imefaulu |
| Remainder families: residue classes that add up | Ukaguzi kamili wa visa vyote vyenye kikomo, Mfano kinzani | imefaulu |
| Checking set identities exhaustively | Ukaguzi kamili wa visa vyote vyenye kikomo, Mfano kinzani | imefaulu |
| Negative times negative: grid, symbols and proof | Ushahidi wa majaribio, Ukokotoaji wa kiishara | imefaulu |
Mapungufu yanayojulikana
- Kuna masomo matano tu na Njia za Maajabu saba; kila mada nyingine imepangwa.
- Uthibitisho wa Lean hutumia kiini cha Lean 4 pekee; kuunganisha Mathlib kumepangwa.
- Mazingira ya Pyodide (kivinjari) na mazingira ya majaribio ya CPython ni matoleo tofauti ya Python; majaribio yalikaguliwa kuona kwamba yanachapisha matokeo yanayofanana, lakini ukaguzi huo bado haujawekwa kiotomatiki.
- Hakuna ukaguzi wa ufikivu uliofanyika.
- Rejista za lugha na nchi zina maingizo yaliyowekewa alama ya ukaguzi.
Maeneo yanayohitaji ukaguzi wa binadamu
- Kila somo, njia, zoezi na suluhisho (usahihi wa kihisabati)
- Ufaafu kwa umri na ualimu, hasa wa nyenzo za Chekechea–Darasa la 2 na Darasa la 3–5
- Madai ya kihistoria na uhusishaji
- Tafsiri zote zilizoandaliwa na mashine na faharasa za istilahi
- Maingizo ya rejista yenye alama ya “inahitaji ukaguzi”
- Uwekaji wa mada na kingo za masharti ya awali kwenye ramani ya mtaala