Cô gái có một cái tên rất Latinh Flaminia Cavallo bạn có thể làm quen qua trang mạng facebook [1].
Bức ảnh này quả là có ý khiêu khích các chàng trai , nhưng cái mà cô nàng này “chào hàng” (nói nhỏ nhé món hàng “kịch độc”) thì chắc sẽ làm các chàng trai phải giật mình . Anh chàng nào hiếu thắng sẽ phẩy tay (nhưng vẫn dè chừng), anh hay sỹ diện hão sẽ nhún vai ra vẻ không biết (nhưng hơi run run),anh nào yếu bóng vía một chút sẽ sợ thực sự mà không dám nhìn thẳng ,còn chăng là một cách làm quen của các anh chàng sẵn sàng chân thành học hỏi.
Mua hay thuê một định lý toán học
Cô nàng Flaminia Cavallo cung cấp dịch vụ trực tuyến- bán các món quà mà các anh chàng có thể mua cho bạn gái mình ,tất nhiên chị em cũng có thể mua để tặng người yêu dấu của mình nhân các ngày đặc biệt như dịp 8-3 này chẳng hạn hay là ngày “va lung tung” “va linh tinh” gì đó.Với giá từ 15 bảng Anh đến 20 bảng Anh bạn có thể sở hữu một định lý tóan học mang tên mình [2].(để làm hàng với bạn gái nghe cũng được đấy chứ?) .Một chứng chỉ giống cái dưới đây sẽ được gửi tới cho bạn
Có điều bạn đừng ngạc nhiên khi phải mua hay thuê một định lý tóan học.Năm 1694 nhà tóan học Thụy sỹ Johann Bernoulli đã từng có thỏa thuận với nhà tóan học Pháp L’Hopital về việc trả 300 franc cho việc sử dụng tùy ý một định lý của ông trong thời gian một năm.
Đây là một dịch vụ được phát triển từ luận án của cô tại đại học Edinburgh (Scottland) dưới sự hướng dẫn của người thày là giáo sư A.Bundy.Lý thuyết ẩn dấu dưới dịch vụ TheoryMine được phát triển từ vài chục năm với viên gạch cuối cùng là luận án của Flaminia. Luận án của cô không những được thương mại hóa ngay mà còn được cất đi để bảo vệ quyền sở hữu trí tuệ -điều vô cùng hiếm hoi với một luận án sinh viên. Thoạt tiên hệ thống TheoryMine sẽ khởi tạo tập hợp các quy tắc suy diễn hình thức.Sau đó nó khởi tạo tiếp các giả thuyết cho các quá trình quy nạp đó và chuyển sang một “bộ lọc” để tìm phản ví dụ cũng như sẽ từ chối một số giả thuyết. Sau cùng với chỗ giả thuyết có được hệ thống sẽ đi tìm chứng minh cho chúng.Số giả thuyết còn lại chưa chứng minh được sẽ là các giả thuyết mở. TheoryMine đảm bảo rằng các định lý phát minh được bởi robot tóan học này chưa từng được công bố ở bất cứ đâu,và chúng được sinh ra từ yêu cầu của người đặt hàng chứ không phải lấy ra từ cơ sở dữ liệu của TheoryMine.Và nếu có một bài báo toán học công bố một định lý trước khám phá của TheoryMine, một tình huống hy hữu khó xảy ra,thì người sở hữu định lý cũ sẽ được gửi tặng thêm hai định lý (với tên của họ). Có điều là –như cô gợi ý-bạn đừng bao giờ hy vọng rằng định lý ấy của bạn sẽ đọat giải thưởng Fields hay Nobel.
Flaminia Cavallo-Thật khả ái và nữ tính
Cúp vàng dành cho Flaminia do Hiệp Hội Scottish Institution of Enterprise’s (SIE) Trao tặng
Prover – Hệ thống chứng minh tự động
50 năm qua xuât hiện nhiều hệ thống chứng minh tự động với các mức độ tiến hóa khác nhau.Bài toán chứng minh tự động vẫn là một trong những bài toán trung tâm của trí tuệ nhân tạo.Nhiều bài toán lớn được chứng minh bằng máy tính (hoặc với sự trợ giúp của máy tính) đó là : Bài toán 4-màu -1976 (được kiểm chứng chặt chẽ lại năm 2005) , giả thuyết Robbins, Giả thuyết Kepler (1998), Trường hợp 17 điểm của giả thuyết Erdős–Szekeres (2006), giả thuyết NP về tam giác phân với trọng tối thiểu (2008),vv. Đáng chú ý nhất là bài toán 4 màu, được chứng minh lại bằng hệ chương trình Coq [3].
Câu chuyện của nhà toán học Bernoulli đáng để ta suy nghĩ.Bạn nghĩ thế nào nếu mỗi lần bạn thực hiện một cuộc gọi điện thoại thành công bạn phải trả bản quyền
cho giải thuật phát hiện lỗi và sửa sai trên các đường truyền viễn thông,cho giải thuật tối ưu mạng ,vv.Nếu thu phí thì các tác giả này sẽ là người giàu có bậc nhất đấy. Bạn có thấy đóng góp của các nhà toán học lớn đến thế nào cho cuộc sống , đó là các cống hiến có tính nhân loại và được dùng miễn phí!!!.Việc thứ hai là liệu có còn việc cho ta hay không khi tất cả các công việc bị robot lấy cả rồi? Chuỵện thứ ba thì rất nghiêm túc –vậy chứng minh là gì nhỉ?
Zonzon507 –Hà Nội
