{"id":"W2100900784","doi":"10.5555/1894483.1894524","title":"A wiki for Mizar: motivation, considerations, and initial prototype","year":2010,"lang":"en","type":"article","venue":"TU/e Research Portal (Eindhoven University of Technology)","topic":"Security and Verification in Computing","field":"Computer Science","cited_by":28,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Alberta","funders":"","keywords":"Computer science; Focus (optics); Field (mathematics); Software engineering; Programming language","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0007084784,0.00007477033,0.0001316404,0.0005120536,0.0005140603,0.00004598542,0.0005634793,0.0002000806,0.00005063587],"category_scores_gemma":[0.0008027205,0.00008966136,0.00003499061,0.0005502608,0.0004979501,0.0003098756,0.0003581101,0.0004579189,0.000007286917],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00001602531,"about_ca_system_score_gemma":0.0002547952,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00008250283,"about_ca_topic_score_gemma":0.0001019033,"domain_scores_codex":[0.9990093,0.00003832661,0.0001455758,0.0003231948,0.0002347332,0.000248936],"domain_scores_gemma":[0.9985352,0.0002754353,0.0000957623,0.0004180823,0.0006088365,0.00006667741],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.00003575637,0.0001389931,0.003485822,0.00005592,0.00003710118,0.00003225911,0.0006700213,0.000004138407,0.008222801,0.9667013,0.003371631,0.01724426],"study_design_scores_gemma":[0.00556891,0.00221805,0.01925691,0.0002219444,0.00003877586,0.0003670393,0.004846558,0.03885938,0.0942361,0.6296361,0.203628,0.001122154],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.9086646,0.00006202734,0.07359529,0.01296821,0.0001483782,0.001535141,0.00001977171,0.0003518032,0.00265479],"genre_scores_gemma":[0.9412976,0.000009819416,0.05854692,0.0000189931,0.00002539487,0.000004998054,0.00000422819,0.000004426953,0.00008763729],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.3370652,"threshold_uncertainty_score":0.3953788,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05854665833522479,"score_gpt":0.3276158500955672,"score_spread":0.2690691917603424,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}