Halmos hakkında

Halmos matematik için bir forumdur. Sunucu matematiki kontrol eder. Bazı yazıların, güvenle yazılmış bir yazının üretmeyeceği bir işaret taşıdığını fark ettiğinize kadar herhangi bir bağlantı toplama sistemi gibi görünür.

Diğer matematik forumlarının sorunu şu ki,

MathOverflow, math.StackExchange, r/math, arXiv yorum bölümleri. Hepsinin doğruluğunu belirleyen tek bir hakem var: diğer insanlar, tartışıyorlar. Bu dikkate değer derecede iyi çalışıyor, ve bu da neden akıcı bir şekilde yazılmış yanlış bir kanıt kötü yazılmış doğru bir kanıtın üstüne çıkıyor, ve neden "ben kontrol ettim" ve "ben inanıyorum" sayfada aynı görünüyor.

Halmos, tartışılamayan ikinci bir hakem ekler.

Sunucunun gerçekte yaptığı şey

Herhangi bir yazıya veya yoruma çitli bir blok koyun ve burada, gönderirken çalışır:

Blok	Ne olacak?	Kazanabilir mi? ∎?
`lean`	Mathlib ile karşılaştırıldı. Kernel kanıt terimi kabul ediyor ya da kabul etmiyor.	Evet
`sage`	SageMath onu çalıştırır; gerçek çıkışı postaya sabitlenir.	Hayır.
`gp`	PARI/GP yönetiyor.	Hayır.
`z3`	Z3 bir model arıyor: en hızlı yol reddet Bir şey.	Hayır.
`python`	Sandboxed Python, çıkış bağlandı.	Hayır.

Blokun altındaki çıktı, aletin yazdırdığı şeydir, sözde. Asla bir özet: özetleme tam olarak bir üretim içine girer.

Nasıl denetleneceğini bir dakikada göstereceğim.

Normal yorum yap. Çoğu yazıda matematik yok ve burada da hiçbir şey matematik gerektiriyor.
Matematikleri çizgi içinde yaz ile $…$ , ya da bir görüntü bloku ile $$…$$. Gerçek bir matematik gibi görünüyor, hiçbir şey yürütülmiyor. Sadece bir işaretleme. Bir tane görüyorum.
Makineye sor. Etiketlenmiş bir çit bloku sage, gp, z3 ya da python is executed here and its output attached to your post, verbatim. That is evidence, not proof. Bir tane görüyorum.
Bir şeyler çiz. ile plot blok (matplotlib, ile plt ve np hazır), ya da bir diziyi oeis: tam sayıları yapıştır ve biliniyorsa isimle geri gelir.
Bir şeyi kanıtla. A-M_BAR_İspanyolca lean blok Mathlib ile tip kontrol edildi. Bunu herhangi bir yoruma yapıştır: Bir tane görüyorum.

```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```

Kayıt sadece bir kullanıcı adı ve şifre ile yapılıyor. E-posta yok, onay adımları yok. Kontrolörlerin şu anda yaptığı her şey internette. kuyruk, ve her kontrolcünün canlı durumu status pageEğer biri düşerse "işleyememiş" denir, hiçbir zaman "reddedilmemiş" demezler.

Kendi hızınızla yazın

Bir yazı başlat Matematikinizi okuyucuların göreceği gibi görmek için yazma ve önizleme arasında geçiş yapabilirsiniz. Değişiklikler otomatik olarak kaydediliyor Yazmalarınızı.; Taslak kaydetme JavaScript olmadan da çalışır. Taslak ve önizleme kodları hiçbir zaman çalıştırmaz. Paylaşmaya hazır olduğunuzda yayınlayın.

Bir makalenin içerik listesini oluşturmak için başlıkları kullanın. Ekle menüsü tanımlar, teoremler, kanıtlar, örnekler, tablolar ve bağlantılar ekler. Örneğin:

:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::

:::proof
Explain your argument here.
:::

Bir kanıt kutusu bir argüman sunuyor; kabul edilen Lean kontrolü doğrulama işaretini sağlar. Düzenleyicinin altında kaynaklar ve özel LaTeX makroları ekleyin veya varsayılanları ayarlayınız profilinizİlgilenen okuyucuların yazınızı bulmaları için bir konu ve etiketler seçin.

Yayınlanan makaleler makaleyi düzenley linkine sahiptir. Kaydedilen düzenlemeler güncellemeyi yayınlayana kadar gizli kalır. Makale adresini korur ve mevcut makine kontrolleri kontrol ettikleri metinle bağlantılı kalır.

Birlikte okumaya devam edin.

Makaleleri özel okuma listenize kaydet ve kişisel bir liste için yazarlar veya konuları takip et Following Mesajlarınıza ve yorumlarınıza verilen cevaplar, Sana cevaplar..

Bir kitap veya dizi oluştur Yayınlanan yazılarınızı birleştirmek için. Bölümler ekle, sıralarını düzenle ve içeriği hazır olduğunda kamuya açık kıl. Özel bir koleksiyon içerik listesini gizler; yazıları tek tek yayınlanmaktadır.

İmza

∎ Buna "a" denir. halmosPaul Halmos'den sonra, kanıt sonu sembolü tanıttı.Bu sitede otoriteyi taşıyan tek şey bu, bu yüzden kasten elde etmek zor.

Sadece Lean bunu ayarlayabilir. True kanıt değil, kanıttır.
sorry, native_decide, Yeni bir axiom, unsafe ve debug.skipKernelTC reddedilirler. önce Dosya çalıştırılıyor, bu yüzden bir hileci hesaplamaya bile gerek duymuyor.
Bir yürütme, onu üreten metne sabitlenir. Mesajı düzenlerseniz, işaret yeni kelimelere aktarılmak yerine eski haline döner.
Eğer bir şahin düşerse, "yürütülemedi"Hiçbir zaman. "reddedildi". Durum kontrolü Bu yüzden kamuya açık.

Topluluklar

Veri doğrulama ucuzdur, keşif ucuz değil. Topluluklar Herkes katkıda bulunabilir, kimse sonuçlara sahip değildir ve her bir çalışması kamuya açıktır, hiçbir yere gitmeyenler de dahil, ki bunlar genellikle bilgilendirici olanlar.

Kim yönetiyor?

Halmos bağımsız ve küçük. Eğer burada bir şey yanlışsa, bunu kanıtlamanın en hızlı yolu sunucunun çalıştırabileceği bir bloktur. İletişime geç.